The 5 Colour Theorem in Isabelle/Isar
Gertrud Bauer and Tobias Nipkow
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.
ps
BibTeX:
@inproceedings{BauerN:2002,author={Gertrud Bauer and Tobias Nipkow},
title={The 5 Colour Theorem in {Isabelle/Isar}},
booktitle={Theorem Proving in Higher Order Logics},
editor={V. Carre{\~n}o and C. Mu{\~n}oz and S. Tahar},
publisher=Springer,series=LNCS,volume=2410,pages={67-82},year=2002}