New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract)
New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract)
复制标题
DOI：
--
复制
发表时间：
2020-04
期刊：
影响因子：
--
通讯作者：
Erika 'Abrah'am;J. Davenport;M. England;Gereon Kremer;Zak Tonks
中科院分区：
文献类型：
--
作者：
Erika 'Abrah'am;J. Davenport;M. England;Gereon Kremer;Zak Tonks
本文的目的是探讨这样一个问题：“在多大程度上我们可以在真实的代数几何中给出形式化的、机器可验证的证明？”“这个问题以前就被问过，但到目前为止，回答这些问题的主要算法还没有正式化。我们提出了一个新的算法，用于确定公式的可满足性的实数通过圆柱代数覆盖[亚伯拉罕，达文波特，英格兰，Kremer，\n {决定的一致性非线性真实的算术约束与冲突驱动程序搜索使用圆柱代数覆盖}，2020]可能提供跟踪和输出，使结果比竞争算法的结果更容易受到机器验证。
The purpose of this paper is to explore the question "to what extent could we produce formal, machine-verifiable, proofs in real algebraic geometry?" The question has been asked before but as yet the leading algorithms for answering such questions have not been formalised. We present a thesis that a new algorithm for ascertaining satisfiability of formulae over the reals via Cylindrical Algebraic Coverings [Abraham, Davenport, England, Kremer, \emph{Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driver Search Using Cylindrical Algebraic Coverings}, 2020] might provide trace and outputs that allow the results to be more susceptible to machine verification than those of competing algorithms.