Document Open Access Logo

Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps

Author Jean-Francois Dufourd



PDF
Thumbnail PDF

File

LIPIcs.STACS.2008.1349.pdf
  • Filesize: 184 kB
  • 12 pages

Document Identifiers

Author Details

Jean-Francois Dufourd

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

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)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail