@MISC{GLIB_015.MIZ,
  AUTHOR = {Koch, Sebastian},
  NOTE1 = {The author is enrolled in the Johannes Gutenberg University in Mayence, Germany},
  TITLE = {About Graph Sums},
  SECTION1 = {Replacing Vertices and Edges},
  SECTION2 = {Graph selectors of Graph-yielding Functions},
  SECTION3 = {Isomorphisms between Graph-membered Sets or Graph-yielding Functions},
  SECTION4 = {Distinguishing the Vertex and Edge Sets of several Graphs from each other},
  SECTION5 = {Distinguishing the Range of a Graph-yielding Function},
  SECTION6 = {The Sum of Graphs},
  SECTION7= {The Sum of two Graphs},
  DAY = {30},
  MONTH = {November},
  YEAR = {2021},
  ADDRESS1 = {Germany\\\href{mailto:skoch02@students.uni-mainz.de}{skoch02@students.uni-mainz.de}},
  SUMMARY = {In this article the sum (or disjoint union) of graphs is formalized in the   Mizar system \cite{FourDecades}, based on the formalization of graphs 
  in \cite {GLIB_000.ABS}.},
  INTRODUCTION = {The sum of graphs has already been formalized in Mizar to a certain   extent in \cite{GLIB_014.ABS}, in the case where the vertices and edges of the graphs   are disjoint. This disjoint union matches the definitions often given in the   literature (cf. \cite{MULTI,HANDBOOK,GERWAG,DIEST}). However, graphs are added   together most of the time without much concern about what kind of objects actually   constitute the vertices and edges. This article's goal is to formalize that practice.   Naturally, in this paper the sum is generalized to families of multidigraphs, i.e. the   graphs of \cite{GLIB_000.ABS}.\par
  The first section introduces functors to replace the concrete objects behind vertices   and edges of a graph with other objects, which will later be used in section 5.\par
  In the second section graph selector variants for \texttt{Graph-yielding} functions   are described in a similar way as it was done for \texttt{Graph-membered} sets in   section 1 of \cite{GLIB_014.ABS}.\par
  Isomorphisms between two \texttt{Graph-membered} sets or two \texttt{Graph-yielding}   functions are formalized in section 3. They are the foundation for isomorphisms   between unions (section 4) and sums (section 6) of graphs.\par
  Section 4 introduces attributes \texttt{vertex-disjoint} and \texttt{edge-disjoint}   for sets or functions of graphs. A lot of attention is given to graph unions of   vertex-disjoint sets of graphs, since these essentially are the graph sums.\par
  The rest of the article then focuses on graph sums that are vertex-disjoint unions of   the range of a function of graphs which is isomorphic to a given graph function not   necessarily vertex-disjoint, so that in future articles authors do not need to create   a vertex-disjoint function themselves. This "canonical" distinction function is   formalized in section 5. A second distinction function is provided that leaves exactly   one graph of the original graph function as it was. Isomorphism theorems between these   two distinction functions and the original functions are provided as well and needed   for the sum isomorphisms in the next section.\par
  Section 6 introduces the mode \texttt{GraphSum} of a (not necessarily vertex-disjoint)   graph function as a graph (directed) isomorphic to the union of the range of the   distinction function. The second distinction function is used to provide a graph sum   that is a supergraph of a given graph in the graph function.\par
  Finally the last section defines the graph sum of two graph as a supergraph of the   first graph using the general definition from section 6.}}

@Article{BancerekJAR:2018,
  author={Bancerek, Grzegorz and Byli{\'{n}}ski, Czes{\l}aw and Grabowski, Adam and Korni{\l}owicz, Artur and Matuszewski, Roman and Naumowicz, Adam and P{\k{a}}k, Karol},
  title={The Role of the {M}izar {M}athematical {L}ibrary for Interactive Proof Development in {M}izar},
  journal={Journal of Automated Reasoning},
  year={2018},
  volume={61},
  number={1},
  pages={9--32},
  doi={10.1007/s10817-017-9440-6},
  url={https://doi.org/10.1007/s10817-017-9440-6}
}
@Article{FourDecades,
  author={Grabowski, Adam and Korni{\l}owicz, Artur and Naumowicz, Adam},
  title={Four Decades of {M}izar},
  journal={Journal of Automated Reasoning},
  year={2015},
  volume={55},
  number={3},
  pages={191--198},
  issn={1573-0670},
  doi={10.1007/s10817-015-9345-1}
}
@book{SIMPLE,
  TITLE = {Introduction to graph theory},
  AUTHOR = {Wilson, Robin James},
  ADDRESS = {Edinburgh},
  PUBLISHER = {Oliver & Boyd},
  YEAR = {1972},
  ISBN = {0-05-002534-1},
  PAGES = {VIII, 168 p.},
  URL = {http://scans.hebis.de/HEBCGI/show.pl?10670775_toc.pdf},
}
@book{GERWAG1,
  TITLE = {Graphentheorie : Anwendung auf Topologie, Gruppentheorie und Verbandstheorie},
  VOLUME = {1. Anwendung auf Topologie, Gruppentheorie und Verbandstheorie},
  AUTHOR = {Wagner, Klaus ; Bodendiek, Rainer},
  ADDRESS = {Mannheim [u.a.]},
  PUBLISHER = {B-I-Wissenschaftsverl.},
  YEAR = {1989},
  ISBN = {3-411-03226-X},
  PAGES = {XV, 252 p.}
}
@book{DIESTEL,
  TITLE = {Graph theory},
  VOLUME = {Graduate texts in mathematics ; 173},
  AUTHOR = {Diestel, Reinhard [Verfasser]},
  ADDRESS = {Berlin},
  PUBLISHER = {Springer},
  YEAR = {[2017]},
  EDITION = {Fifth edition},
  ISBN = {978-3-662-53621-6},
  PAGES = {XVIII, 428 p.}
}
@book{MULTI,
  TITLE = {Graph theory},
  SERIES = {Graduate texts in mathematics ; 244},
  AUTHOR = {Bondy, John Adrian ; Murty, U. S. R.},
  ADDRESS = {New York, NY},
  PUBLISHER = {Springer},
  YEAR = {2008},
  ISBN = {978-1-84628-969-9},
  PAGES = {XII, 652 p.},
  URL = {http://scans.hebis.de/HEBCGI/show.pl?19542627_toc.pdf ; http://scans.hebis.de/HEBCGI/show.pl?19542627_kap-2.pdf ; http://scans.hebis.de/HEBCGI/show.pl?19542627_ein-1.pdf}
}
@book{HANDBOOK,
  title = {Handbook of discrete and combinatorial mathematics},
  series = {Discrete mathematics and its applications},
  editor = {Rosen, Kenneth H. [Herausgeber]},
  address = {Boca Raton},
  publisher = {CRC Press},
  year = {[2018]},
  edition = {Second edition},
  ISBN = {978-1-58488-780-5},
  pages = {XXIV, 1590 p.},
}