The 5 Colour Theorem in Isabelle/Isar

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.

• Type: Conference
• Year: 2002
• Where: TPHOL
• Authors: Gertrud Bauer, Tobias Nipkow
• Keywords: Automated Reasoning, Colour Theorem, Inductive Definition, TPHOL 2002, Undirected Planar Graphs