10.4230/LIPICS.STACS.2008.1349
Dufourd, Jean-Francois
Jean-Francois
Dufourd
Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2008
Article
Formal specifications
Computational topology
Computer-aided proofs
Coq
Planar subdivisions
Hypermaps
Jordan Curve Theorem
Albers, Susanne
Susanne
Albers
Weil, Pascal
Pascal
Weil
2008
2008-02-06
2008-02-06
2008-02-06
en
urn:nbn:de:0030-drops-13493
10.4230/LIPIcs.STACS.2008
978-3-939897-06-4
1868-8969
10.4230/LIPIcs.STACS.2008
LIPIcs, Volume 1, STACS 2008
25th International Symposium on Theoretical Aspects of Computer Science
2013
1
23
253
264
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Albers, Susanne
Susanne
Albers
Weil, Pascal
Pascal
Weil
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2008
1
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
12 pages
189069 bytes
application/pdf
Creative Commons Attribution-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
This paper presents a formalized proof of a discrete form of the
Jordan Curve Theorem. It is based on a hypermap model of planar
subdivisions, formal specifications and proofs assisted by the Coq
system. Fundamental properties are proven by structural or
noetherian induction: Genus Theorem, Euler's Formula, constructive
planarity criteria. A notion of ring of faces is inductively
defined and a Jordan Curve Theorem is stated and proven for any
planar hypermap.
LIPIcs, Vol. 1, 25th International Symposium on Theoretical Aspects of Computer Science, pages 253-264