Skip to main content
SpringerLink
Log in
Book cover

International Conference on Theorem Proving in Higher Order Logics

TPHOLs 2002: Theorem Proving in Higher Order Logics pp 67–82Cite as

The 5 Colour Theorem in Isabelle/Isar

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2410))

Abstract

Based on an inductive definition of triangulations, a theory of undirected planar graphs is developed in Isabelle/HOL. The proof of the 5 colour theorem is discussed in some detail, emphasizing the readability of the computer assisted proofs.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. K. Appel and W. Haken. Every planar map is four colourable. Bulletin of the American mathematical Society, 82:711–112, 1977.

    Article  MathSciNet  Google Scholar 

  2. K. Appel and W. Haken. Every planar map is four colourable. I: Discharging. Illinois J. math., 21:429–490, 1977.

    MATH  MathSciNet  Google Scholar 

  3. K. Appel and W. Haken. Every planar map is four colourable. II: Reducibility. Illinois J. math., 21:491–567, 1977.

    MATH  MathSciNet  Google Scholar 

  4. K. Appel and W. Haken. Every planar map is four colourable, volume 98. Contemporary Mathematics, 1989.

    Google Scholar 

  5. G. D. Birkhoff. The reducibility of maps. Amer. J. Math., 35:114–128, 1913.

    Article  MathSciNet  Google Scholar 

  6. 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–176, 1994.

    Google Scholar 

  7. R. Diestel. Graph Theory. Graduate Texts in Mathematics. Springer, 2000. Electronic Version: http://www.math.uni-hamburg.de/home/diestel/books/graph.theory/.

  8. T. Emden-Weinert, S. Hougardy, B. Kreuter, H. Prömel, and A. Steger. Einführung in Graphen und Algorithmen, 1996. http://www.informatik.hu-berlin.de/Institut/struktur/algorithmen/ga/.

  9. H. Heesch. Untersuchungen zum Vierfarbenproblem. Number 810/a/b in Hochschulskriptum. Bibliographisches Institut, Mannheim, 1969.

    MATH  Google Scholar 

  10. T. Nipkow, L. Paulson, and M. Wenzel. Isabelle/HOL — A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. To appear.

    MATH  Google Scholar 

  11. N. Robertson, D. Sanders, P. Seymour, and R. Thomas. The four colour theorem. http://www.math.gatech.edu/~thomas/FC/fourcolor.html, 1995.

  12. 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–25, 1996.

    Article  MathSciNet  Google Scholar 

  13. N. Robertson, D. Sanders, P. Seymour, and R. Thomas. The four colour theorem. J. Combin. Theory Ser. B, 70:2–44, 1997.

    Article  MATH  MathSciNet  Google Scholar 

  14. M. Wenzel. Isabelle/Isar— A Versatile Environment for Human-Readable Formal Proof Documents. PhD thesis, Institut für Informatik, Technische Universität München, 2002. http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.htm.

  15. D. West. Introduction to Graph Theory. Prentice Hall, New York, 1996.

    MATH  Google Scholar 

  16. F. Wiedijk. The Four Color Theorem Project. http://www.cs.kun.nl/~freek/4ct/, 2000.

  17. 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–409. IEEE Computer Society Press, 1992.

    Google Scholar 

  18. 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–384, 1995.

    Google Scholar 

  19. 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–496, 1998.

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Technische Universität München, Arcisstrasse 21, 80290, München, Germany

    Gertrud Bauer & Tobias Nipkow

Authors
  1. Gertrud Bauer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tobias Nipkow
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. NASA Langley Research Center, MS 130, Hampton, VA, 23681, USA

    Victor A. Carreño

  2. ICASE-Langley Research Center, MS 132C, Hampton, VA, 23681, USA

    César A. Muñoz

  3. Electrical and Computer Engineering, Concordia University, 1455 de Maisonneuve Blvd.W., Montréal, Québec, H3G 1M8, Canada

    Sofiène Tahar

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bauer, G., Nipkow, T. (2002). The 5 Colour Theorem in Isabelle/Isar. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2002. Lecture Notes in Computer Science, vol 2410. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45685-6_6

Download citation

  • DOI: https://doi.org/10.1007/3-540-45685-6_6

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-44039-0

  • Online ISBN: 978-3-540-45685-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation