Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof
From MaRDI portal
Publication:944364
DOI10.1016/j.tcs.2008.02.012zbMath1154.68100OpenAlexW2012142654MaRDI QIDQ944364
Publication date: 16 September 2008
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2008.02.012
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (8)
Tests and proofs for custom data generators ⋮ Formalizing the Face Lattice of Polyhedra ⋮ An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps ⋮ Formal specification and proofs for the topology and classification of combinatorial surfaces ⋮ Designing and proving correct a convex hull algorithm with hypermaps in Coq ⋮ Formal study of functional orbits in finite domains ⋮ Unnamed Item ⋮ Tests and Proofs for Enumerative Combinatorics
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Formal specification of topological subdivisions using hypermaps
- Topological models for boundary representation: A comparison with \(n\)- dimensional generalized maps
- Axioms and hulls
- An axiomatic approach to robust geometric programs
- Formalizing mathematics in higher-order logic: A case study in geometric modelling
- Functional specification and prototyping with oriented combinatorial maps
- A combinatorial analog of the Jordan Curve Theorem
- Formalizing generalized maps in Coq
- Formalizing the trading theorem in Coq
- The axioms of constructive geometry
- Design and formal proof of a new optimal image segmentation program with hypermaps
- Combinatorial Oriented Maps
This page was built for publication: Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof
