@MISC{GLIB_009.MIZ,
  AUTHOR = {Koch, Sebastian},
  NOTE1 = {The author is enrolled in the Johannes Gutenberg University in Mayence, Germany},
  TITLE = {Underlying Simple Graphs},
  SECTION1 = {Preliminaries},
  SECTION2 = {Plain Graphs},
  SECTION3 = {Graphs with Loops Removed},
  SECTION4 = {Graphs with Parallel Edges Removed},
  SECTION5 = {Graphs with Loops and Parallel Edges Removed},
  DAY = {29},
  MONTH = {August},
  YEAR = {2019},
  ADDRESS1 = {Germany\\\href{mailto:skoch02@students.uni-mainz.de}{skoch02@students.uni-mainz.de}},
  SUMMARY = {In the Mizar Mathematical Library\cite{BancerekJAR:2018} there are several formalizations of     graphs with a varying degree of generality, see 
  \cite{TREES_1.ABS,GRAPH_1.ABS,SGRAPH1.ABS,GLIB_000.ABS,SCMYCIEL.ABS}. The \texttt{GLIB\_} series (starting   with \cite{GLIB_000.ABS}) formalizes general digraphs (that is, digraphs with loops and parallel edges   allowed) in Mizar\cite{FourDecades} and provides a rich notation so that any digraph in Mizar can be seen   as an undirected graph simply by ignoring the direction of the edges (although they are always there). In   conclusion, there is no need for another formalization of undirected graphs, in contrast to how it is   typically done in the literature (cf. \cite{SIMPLE,SELECTED}), and the underlying (undirected) graph of a   digraph (in the sense of \cite{GLIB_000.ABS}) is itself. For undirected graphs or digraphs possibly   containing loops and multiple parallel edges, the underlying (simple) graph or digraph is derived by   removing the loops and replacing each set of parallel edges with a single edge. That concept requires   formalization and this article provides subgraph modes that respectively remove loops, (directed) parallel   edges or both from a given (di)graph. "Much of graph theory is concerned with the study of simple   graphs"\cite[p.~3]{MULTI} which results in many books only studying simple graphs, even when graphs are   more generally introduced in the respective book (for example \cite{GERWAG}). The aim of this article was   to ease the transition from simple graphs to general graphs in the formalization process of graph theory   in Mizar.\par
  In addition to the notion of underlying graphs this article also introduces plain graphs, i.e. graphs   without decorators as introduced in \cite{GLIB_003.ABS}. This is important for building sets consisting of   graphs fulfilling certain properties. The set of all loops of a graph is formally introduced as well.
  }}

@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{GERWAG,
  title = {Graphentheorie},
  series = {B.I-Hochschultaschenbücher ; 248},
  author = {Wagner, Klaus},
  address = {Mannheim [u.a.]},
  publisher = {Bibliograph. Inst.},
  year = {1970},
  ISBN = {3-411-00248-4},
  pages = {220 S.}
}
@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 S.},
  URL = {http://scans.hebis.de/HEBCGI/show.pl?10670775_toc.pdf},
}
@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 S.},
  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{SELECTED,
  TITLE = {Selected topics in graph theory},
  EDITOR = {Beineke, Lowell W.},
  ADDRESS = {London [et al.]},
  PUBLISHER = {Academic Press},
  YEAR = {1978},
  ISBN = {0-12-086250-6},
  pages = {IX, 451 S.}
}