Sciweavers

TPHOL
2002
IEEE

The 5 Colour Theorem in Isabelle/Isar

14 years 4 months ago
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.
Gertrud Bauer, Tobias Nipkow
Added 16 Jul 2010
Updated 16 Jul 2010
Type Conference
Year 2002
Where TPHOL
Authors Gertrud Bauer, Tobias Nipkow
Comments (0)