This paper presents a formally verified quantifier elimination (QE) algorithm for first-order real arithmetic by linear and quadratic virtual substitution (VS) in Isabelle/HOL. The Tarski-Seidenberg theorem established that the first-order logic of real arithmetic is decidable by QE. However, in practice, QE algorithms are highly complicated and often combine multiple methods for performance. VS is a practically successful method for QE that targets formulas with low-degree polynomials. To our knowledge, this is the first work to formalize VS for quadratic real arithmetic including inequalities. The proofs necessitate various contributions to the existing multivariate polynomial libraries in Isabelle/HOL, including a method for re-indexing variables in a polynomial. Our framework is modularized and easily expandable (to facilitate integrating future optimizations), and could serve as a basis for developing a general-purpose QE algorithm. Further, as our formalization is designed with practicality in mind, we export our development to SML and test the resulting code on 378 benchmarks from the literature, comparing to Redlog, Z3, Mathematica, and SMT-RAT.
翻译:本文介绍了在伊莎贝尔/HOL中通过线性和二次虚拟替代(VS)进行一阶实际算术的经正式核实的量化除去(QE)算法。 Tarski-Seidenberg 理论认为,真实算术的第一阶逻辑可以由QE来分解。 然而,在实践中,QE算法非常复杂,而且往往结合多种性能方法。 VS是QE中以低度多度多元性计算公式为对象的一个实际成功的量化除去(QE)算法。 据我们所知,这是将VS正规化为四阶性真实算术(包括不平等)的首次工作。 证据证明要求为伊莎贝尔/HOL现有的多变量多元性多元性多数值图书馆做出各种贡献,包括多数值变量再索引法。 我们的框架是模块化的,易于扩展(以便利未来的优化),并且可以作为制定通用的QE算法的基础。 此外,由于我们的正规化设计是实用性的,我们把发展输出给SML,并测试从文献中得出的378个基准,从RMA、MA和SZ3、SMAmatal测试。