#### 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}