论文标题
正式证明真实几何形状的新机会？
New Opportunities for the Formal Proof of Computational Real Geometry?
论文作者
论文摘要
本文的目的是探讨一个问题：“我们在多大程度上可以在多大程度上产生实际代数几何形状的正式，可验证的证据？”以前提出过这个问题，但是到目前为止，回答此类问题的主要算法尚未正式化。我们介绍了一篇论文，即通过圆柱代数覆盖物来确定公式对真实的满意度的新算法[Ábrahám，英格兰，英格兰，克雷默，\ emph {确定非线性的实际算术范围允许使用canlindrical coverne coffers coption} 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 [Ábrahám, 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.
