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

Dufourd, Jean-Francois

doi:10.4230/LIPIcs.STACS.2008.1349

Document

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

Author Jean-Francois Dufourd

Part of: Volume: 25th International Symposium on Theoretical Aspects of Computer Science (STACS 2008)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: Symposium on Theoretical Aspects of Computer Science (STACS)
License: Creative Commons Attribution-NoDerivs 3.0 Unported license
Publication Date: 2008-02-06

PDF

File

PDF

LIPIcs.STACS.2008.1349.pdf

Filesize: 184 kB
12 pages

Document Identifiers

DOI: 10.4230/LIPIcs.STACS.2008.1349
URN: urn:nbn:de:0030-drops-13493

Subject Classification

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

0

Metadata Views

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.

Cite As Get 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

Author Details

Jean-Francois Dufourd

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail