View Related Documents

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.

Fulltext Preview

Image of the first page of the fulltext document