Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof

This article presents formalized intuitionistic proofs for the polyhedra genus theorem, the Euler formula and a sufficient condition of planarity. They are based on a hypermap model for polyhedra and on formal specifications in the Calculus of Inductive Constructions. First, a type of free maps is inductively defined from three atomic constructors. Next, a hierarchy of types defined by invariants, with operations constrained by preconditions, is built on the free maps: hypermaps, oriented combinatorial maps, and a central notion of quasi-hypermaps. Besides, the proofs of their properties are established until the genus theorem and the Euler formula, mainly using a simple induction principle based on the free map term algebra. Finally, a constructive sufficient condition for polyhedra to be planar is set and proved. The whole process is assisted by the interactive Coq proof system. Key words: polyhedra, hypermaps, genus, Euler formula, formal specifications, computer-aided proofs, Coq ...

• Type: Journal
• Year: 2008
• Where: TCS
• Authors: Jean-François Dufourd
• Keywords: Euler Formula, Free Map, Polyhedra, TCS 2008, Theoretical Computer Science