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

Simple item page
dc.creatorDufourd, Jean-François
dc.date2008-02-20
dc.date.accessioned2026-07-07T09:22:03Z
dc.date.available2026-07-07T09:22:03Z
dc.descriptionThis 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.
dc.identifierhttps://arxiv.org/abs/0802.2853
dc.identifierhttp://arxiv.org/abs/0802.2853
dc.identifierDans Proceedings of the 25th Annual Symposium on the Theoretical Aspects of Computer Science - STACS 2008, Bordeaux : France (2008)
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/155240
dc.subjectLogic in Computer Science
dc.subjectDiscrete Mathematics
dc.titleDiscrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps
dc.typetext

Files

Collections

arXiv