@MISC{GLCOLO00.MIZ,
  AUTHOR = {Koch, Sebastian},
  TITLE = {Introduction to Graph Colorings},
  SECTION1 = {Vertex Colorings},
  SECTION2 = {Edge Colorings},
  SECTION3 = {Total Colorings},
  DAY = {23},
  MONTH = {July},
  YEAR = {2022},
  ADDRESS1 = {Germany\\\href{mailto:skoch02@students.uni-mainz.de}{skoch02@students.uni-mainz.de}},
  SUMMARY = {In this article vertex, edge and total colorings of graphs are formalized in the Mizar system \cite{FourDecades}, based on the formalization of graphs in \cite{GLIB_000.ABS}.},
  INTRODUCTION = {Graph coloring has a long history in mathematics and is introduced in almost   every introductionary book on graph theory (cf. \cite{MULTI}, \cite{SIMPLE}, cite{DIESTEL}). In   this article, the basic notions of vertex, edge and total colorings of graphs are formalized 
  in sections 1, 2 and 3 respectively. These sections have the same basic structure.\par
  At first the (not necessarily proper) coloring is defined as a function defined on the vertices   or edges of a graph. The total coloring of a graph is defined as a pair of the other two.\par
  The next definition is about proper colorings, i.e. that no two adjacent vertices or edges are   colored the same. A proper total coloring also requires that vertices and edges who are incident   with each other are not colored the same as well. In the context of this formalization, 
  the vertex of a loop is considered adjacent to itself, but the edge of a loop is not considered   adjacent to itself.\par
  After that an attribute for proper colorability with a cardinal amount of colors is provided. It   is important to note that the definition expresses how many colors are sufficient. Given that     cardinalities can be infinite, an attribute indicating that only finitely many colors are needed   is given as well.\par
  In the last part of each section the chromatic number or index is introduced, indicating how     many colors are at least necessary for a proper coloring.}}
  
@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{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}
}
