Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermapsReportar como inadecuado




Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 LSIIT - Laboratoire des Sciences de l-Image, de l-Informatique et de la Télédétection

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





Autor: Jean-François Dufourd -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados