LIPIcs.STACS.2008.1349.pdf
- Filesize: 184 kB
- 12 pages
Document
Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps
Author
-
Part of:
Volume:
25th International Symposium on Theoretical Aspects of Computer Science (STACS 2008)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Symposium on Theoretical Aspects of Computer Science (STACS) - License:
Creative Commons Attribution-NoDerivs 3.0 Unported license
- Publication Date: 2008-02-06
Cite AsGet BibTex
Jean-Francois Dufourd. Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps. In 25th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 1, pp. 253-264, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)
https://doi.org/10.4230/LIPIcs.STACS.2008.1349
https://doi.org/10.4230/LIPIcs.STACS.2008.1349
Abstract
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.
Keywords
- Formal specifications
- Computational topology
- Computer-aided proofs
- Coq
- Planar subdivisions
- Hypermaps
- Jordan Curve Theorem
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads