离散Jordan曲线定理：用hypermaps在Coq中形式化证明
计算机科学中的逻辑
2008-02-21 v1 离散数学
摘要
本文给出了一个离散形式的Jordan曲线定理的形式化证明。该证明基于平面细分的hypermap模型，借助Coq系统进行形式化规范和证明辅助。通过结构归纳或Noetherian归纳证明了基本性质：亏格定理、Euler公式、构造性平面性判据。归纳定义了面的环的概念，并针对任意平面hypermap陈述并证明了Jordan曲线定理。
引用
@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}
}