@MISC{GLPACY00.MIZ,
  AUTHOR = {Koch, Sebastian},
  TITLE = {About Path and Cycle Graphs},
  SECTION1 = {Preliminaries},
  SECTION2 = {Path Graphs},
  SECTION3 = {Cycle Graphs},
  DAY = {9},
  MONTH = {December},
  YEAR = {2024},
  ADDRESS1 = {Germany\\\href{mailto:fly.high.android@gmail.com}{fly.high.android@gmail.com}},
  SUMMARY = {In this article path and cycle graphs are formalized in the Mizar system.},
  INTRODUCTION = {Path and cycle graphs are two fundamental graph families (cf. \cite{MULTI}, \cite{SIMPLE}, cite{DIESTEL}).
  In this article both types are formalized in the Mizar system \cite{FourDecades} (based on the formalization of graphs in \cite{GLIB_000.ABS}),
  in a way that also includes the 1-cycle, 2-cycle, ray and double-ray graph in the definitions. It is shown
  how a finite path graph can be constructed successively and how to construct cycle graphs from finite path graphs.
  A maximal graph path is characterized for every path graph, as well. Furthermore, the rather obvious fact that a graph circuit
  in a cycle graph covers all its vertices and edges is proven and constitutes the longest proof in this work.
}}

@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 and 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}
}