{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:11:30Z","timestamp":1725484290564},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540440390"},{"type":"electronic","value":"9783540456858"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45685-6_6","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T16:47:53Z","timestamp":1179593273000},"page":"67-82","source":"Crossref","is-referenced-by-count":6,"title":["The 5 Colour Theorem in Isabelle\/Isar"],"prefix":"10.1007","author":[{"given":"Gertrud","family":"Bauer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tobias","family":"Nipkow","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,25]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","first-page":"711","DOI":"10.1090\/S0002-9904-1976-14122-5","volume":"82","author":"K. Appel","year":"1977","unstructured":"K. Appel and W. Haken. Every planar map is four colourable. Bulletin of the American mathematical Society, 82:711\u2013112, 1977.","journal-title":"Bulletin of the American mathematical Society"},{"key":"6_CR2","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1215\/ijm\/1256049011","volume":"21","author":"K. Appel","year":"1977","unstructured":"K. Appel and W. Haken. Every planar map is four colourable. I: Discharging. Illinois J. math., 21:429\u2013490, 1977.","journal-title":"Illinois J. math."},{"key":"6_CR3","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1215\/ijm\/1256049012","volume":"21","author":"K. Appel","year":"1977","unstructured":"K. Appel and W. Haken. Every planar map is four colourable. II: Reducibility. Illinois J. math., 21:491\u2013567, 1977.","journal-title":"Illinois J. math."},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"K. Appel and W. Haken. Every planar map is four colourable, volume 98. Contemporary Mathematics, 1989.","DOI":"10.1090\/conm\/098"},{"key":"6_CR5","doi-asserted-by":"publisher","first-page":"114","DOI":"10.2307\/2370276","volume":"35","author":"G. D. Birkhoff","year":"1913","unstructured":"G. D. Birkhoff. The reducibility of maps. Amer. J. Math., 35:114\u2013128, 1913.","journal-title":"Amer. J. Math."},{"key":"6_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1007\/3-540-58450-1_41","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"C.-T. Chou","year":"1994","unstructured":"C.-T. Chou. A Formal Theory of Undirected Graphs in Higher-Order Logic. In T. Melham and J. Camilleri, editors, Higher Order Logic Theorem Proving and Its Applications, volume 859 of LNCS, pages 158\u2013176, 1994."},{"key":"6_CR7","unstructured":"R. Diestel. Graph Theory. Graduate Texts in Mathematics. Springer, 2000. Electronic Version: http:\/\/www.math.uni-hamburg.de\/home\/diestel\/books\/graph.theory\/ ."},{"key":"6_CR8","unstructured":"T. Emden-Weinert, S. Hougardy, B. Kreuter, H. Pr\u00f6mel, and A. Steger. Einf\u00fchrung in Graphen und Algorithmen, 1996. http:\/\/www.informatik.hu-berlin.de\/Institut\/struktur\/algorithmen\/ga\/ ."},{"key":"6_CR9","volume-title":"Untersuchungen zum Vierfarbenproblem","author":"H. Heesch","year":"1969","unstructured":"H. Heesch. Untersuchungen zum Vierfarbenproblem. Number 810\/a\/b in Hochschulskriptum. Bibliographisches Institut, Mannheim, 1969."},{"key":"6_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"T. Nipkow, L. Paulson, and M. Wenzel. Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. To appear."},{"key":"6_CR11","unstructured":"N. Robertson, D. Sanders, P. Seymour, and R. Thomas. The four colour theorem. http:\/\/www.math.gatech.edu\/~thomas\/FC\/fourcolor.html , 1995."},{"issue":"1","key":"6_CR12","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1090\/S1079-6762-96-00003-0","volume":"2","author":"N. Robertson","year":"1996","unstructured":"N. Robertson, D. Sanders, P. Seymour, and R. Thomas. A new proof of the four colour theorem. Electron. Res. Announce. Amer. Math Soc., 2(1):17\u201325, 1996.","journal-title":"Electron. Res. Announce. Amer. Math Soc."},{"key":"6_CR13","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/jctb.1997.1750","volume":"70","author":"N. Robertson","year":"1997","unstructured":"N. Robertson, D. Sanders, P. Seymour, and R. Thomas. The four colour theorem. J. Combin. Theory Ser. B, 70:2\u201344, 1997.","journal-title":"J. Combin. Theory Ser. B"},{"key":"6_CR14","unstructured":"M. Wenzel. Isabelle\/Isar\u2014 A Versatile Environment for Human-Readable Formal Proof Documents. PhD thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, 2002. http:\/\/tumb1.biblio.tu-muenchen.de\/publ\/diss\/in\/2002\/wenzel.htm ."},{"key":"6_CR15","volume-title":"Introduction to Graph Theory","author":"D. West","year":"1996","unstructured":"D. West. Introduction to Graph Theory. Prentice Hall, New York, 1996."},{"key":"6_CR16","unstructured":"F. Wiedijk. The Four Color Theorem Project. http:\/\/www.cs.kun.nl\/~freek\/4ct\/ , 2000."},{"key":"6_CR17","unstructured":"W. Wong. A simple graph theory and its application in railway signalling. In M. Archer, J. Joyce, K. Levitt, and P. Windley, editors, Proc. 1991 International Workshop on the HOL Theorem Proving System and its Applications, pages 395\u2013409. IEEE Computer Society Press, 1992."},{"key":"6_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/3-540-60275-5_77","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"M. Yamamoto","year":"1995","unstructured":"M. Yamamoto, S.-y. Nishizaha, M. Hagiya, and Y. Toda. Formalization of Planar Graphs. In E. Schubert, P. Windley, and J. Alves-Foss, editors, Higher Order Logic Theorem Proving and Its Applications, volume 971 of LNCS, pages 369\u2013384, 1995."},{"key":"6_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/BFb0055153","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Yamamoto","year":"1998","unstructured":"M. Yamamoto, K. Takahashi, M. Hagiya, S.-y. Nishizaki, and T. Tamai. Formalization of Graph Search Algorithms and Its Applications. In J. Grundy and M. Newey, editors, Theorem Proving in Higher Order Logics, volume 1479 of LNCS, pages 479\u2013496, 1998."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45685-6_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T01:38:12Z","timestamp":1556415492000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45685-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440390","9783540456858"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-45685-6_6","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}