@MISC{GLUNIR00.MIZ,
  AUTHOR = {Koch, Sebastian},
  NOTE1 = {The author is enrolled in the Johannes Gutenberg University in Mayence, Germany},
  TITLE = {Unification of Graphs and Relations in {M}izar},
  SECTION1 = {The Adjacency Relation},
  SECTION2 = {Create non-Dmulti Graphs from Relations},
  SECTION3 = {Create non-multi Graphs from symmetric Relations},
  DAY = {31},
  MONTH = {May},
  YEAR = {2020},
  ADDRESS1 = {Germany\\\href{mailto:skoch02@students.uni-mainz.de}{skoch02@students.uni-mainz.de}},
  SUMMARY = {A (di)graph without parallel edges can simply be represented by a binary relation of the vertices and on the other hand, any binary relation can be expressed as such a graph. In this article, this correspondence is formalized in the Mizar system\cite{FourDecades}, based on the formalization of graphs in \cite{GLIB_000.ABS} and relations in \cite{RELAT_1.ABS,RELSET_1.ABS}. Notably, a new definition of \texttt{createGraph} will be given, taking only a non empty set $V$ and a binary relation $E\subseteq V\times V$ to create a (di)graph without parallel edges, which will provide to be very useful in future articles.},
  INTRODUCTION = {Digraphs without multiple edges can be represented by binary relations 
  (cf. \cite{AGT}) and this is in fact the way they are usually defined in textbooks 
  which are primarly concerned about graphs without multiple edges 
  (cf. \cite{SIMPLE,HOMO,GRELAT}). While a mathematician can switch between these 
  representations without problems, due to its pedantic nature the Mizar system 
  \cite{FourDecades} needs a formalization of this change of viewpoint, which is 
  provided by this article. In the Mizar Mathematical Library \cite{BancerekJAR:2018} 
  this problem hasn't been adressed yet, although the undirected analogon can be 
  found as an alternative definition for simple graphs in \cite{SGRAPH1.ABS} 
  (which isn't used anywhere else) and the friendship theorem was formalized 
  in \cite{FRIENDS1.ABS} using only relations.\par
  In the first section the dominance and adjacency relation of a graph $G$ are 
  rigorously introduced. $G$ isn't required to be without parallel edges for this, 
  therefore the relations of $G$ and the graph given by removing parallel edges 
  (directed parallel for the dominance) as defined in \cite{GLIB_009.ABS} are 
  the same.\par
  The second section introduces the new functor definition for \texttt{createGraph}, 
  taking a non empty set $V$ and a relation $E\subseteq V\times V$ and returning 
  a graph representing this relation. It is shown that the graph created this 
  way from a dominance relation of a graph $G$ without directed parallel edges is 
  directed isomorphic to $G$ itself.\par
  Since undirected graphs are sometimes viewed as symmetric digraphs 
  (cf. \cite{HOMO,AGT,GRELAT}, the last section introduces a mode getting a graph 
  without parallel edges of any kind by simply removing them from the functor result 
  of the previous section. Similar to before, it is shown that the graph created this 
  way from an adjacency relation of a graph $G$ without parallel edges is isomorphic 
  to $G$ itself.}}

@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 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{HOMO,
  title = {Graphs and homomorphisms},
  series = {Oxford lecture series in mathematics and its applications ; 28},
  author = {Hell, Pavol ; Nesetril, Jaroslav},
  address = {Oxford},
  publisher = {Oxford Univ. Press},
  year = {2004},
  ISBN = {0-19-852817-5},
  pages = {IX, 244 S.},
  url = {http://scans.hebis.de/HEBCGI/show.pl?12385357_toc.pdf}
}
@book{GRELAT,
  title={Relations and graphs: discrete mathematics for computer scientists},
  author={Schmidt, Gunther and Str{\"o}hlein, Thomas},
  year={2012},
  publisher={Springer Science \& Business Media}
}
@book{AGT,
  title={Algebraic graph theory: morphisms, monoids and matrices},
  author={Knauer, Ulrich},
  volume={41},
  year={2011},
  publisher={Walter de Gruyter}
}