An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
From MaRDI portal
Publication:839032
DOI10.1007/s10817-009-9117-xzbMath1187.68525OpenAlexW2046255686MaRDI QIDQ839032
Publication date: 1 September 2009
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-009-9117-x
formal specificationscomputational topologyCoq systemcomputer-aided proofscombinatorial hypermapsdiscrete Jordan curve theoremplanar subdivisions
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (6)
Tests and proofs for custom data generators ⋮ Verification of Closest Pair of Points Algorithms ⋮ 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 ⋮ 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
- Discrete Jordan curve theorems
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Formal proof of a program: find
- Explaining Gabriel-Zisman localization to the computer
- Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof
- A definition of surfaces of \({\mathbb{Z}}^{3}\). A new 3D discrete Jordan theorem
- Functional specification and prototyping with oriented combinatorial maps
- A digital analogue of the Jordan curve theorem
- A combinatorial analog of the Jordan Curve Theorem
- Digital pseudomanifolds, digital weakmanifolds and Jordan--Brouwer separation theorem
- Formalizing the trading theorem in Coq
- Design and formal proof of a new optimal image segmentation program with hypermaps
- Combinatorial Oriented Maps
- The Jordan Curve Theorem, Formally and Informally
- Theorem Proving in Higher Order Logics
This page was built for publication: An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
