计算实几何形式化证明的新机遇？
符号计算
2021-06-17 v1 计算机科学中的逻辑
摘要
本文旨在探讨“我们在多大程度上能为实代数几何中的命题生成形式化、机器可验证的证明？”这一问题。该问题此前已被提出，但迄今为止用于回答此类问题的主流算法尚未被形式化。我们提出一个论点：一种通过柱形代数覆盖判定实数上公式可满足性的新算法[Ábrahám, Davenport, England, Kremer, 《使用柱形代数覆盖的冲突驱动搜索判定非线性实算术约束的一致性》, 2020]可能提供追踪信息与输出，使得其结果比竞争算法的结果更易受机器验证。
引用
@article{arxiv.2004.04034,
title = {New Opportunities for the Formal Proof of Computational Real Geometry?},
author = {Erika {Á}brahám and James Davenport and Matthew England and Gereon Kremer and Zak Tonks},
journal= {arXiv preprint arXiv:2004.04034},
year = {2021}
}