Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps
Logic in Computer Science
2008-02-21 v1 Discrete Mathematics
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
@article{arxiv.0802.2853,
title = {Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps},
author = {Jean-François Dufourd},
journal= {arXiv preprint arXiv:0802.2853},
year = {2008}
}