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

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

2008-02-20

arxiv.org/abs/0802.2853v1

Dans Proceedings of the 25th Annual Symposium on the Theoretical Aspects of Computer Science - STACS 2008, Bordeaux : France (

Computer Science

Logic in Computer Science

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-647833