Sciweavers

Share
TCS
2008

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

8 years 5 months ago
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 ...
Jean-François Dufourd
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2008
Where TCS
Authors Jean-François Dufourd
Comments (0)
books