几何算法的形式化验证：Coq 证明中抽象视图与对称性的探寻
计算机科学中的逻辑
2018-09-05 v1 计算几何
摘要
本扩展摘要关于构建三角剖分算法形式化描述的一项工作，始于该算法的朴素描述，其中三角形、边和三角剖分仅被给定为集合，最复杂的概念是边界边与分离边。在对这一算法进行证明时，对称性问题浮现出来，本论述试图说明这些对称性应如何处理。所有工作均依赖于使用 Coq 与 mathematical components 库所完成的形式化开发。
引用
@article{arxiv.1809.00559,
title = {Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs},
author = {Yves Bertot},
journal= {arXiv preprint arXiv:1809.00559},
year = {2018}
}