We formalize a multivariate quantifier elimination (QE) algorithm in the theorem prover Isabelle/HOL. Our algorithm is complete, in that it is able to reduce any quantified formula in the first-order logic of real arithmetic to a logically equivalent quantifier-free formula. The algorithm we formalize is a hybrid mixture of Tarski's original QE algorithm and the Ben-Or, Kozen, and Reif algorithm, and it is the first complete multivariate QE algorithm formalized in Isabelle/HOL.

翻译：我们在理论证明者Isabelle/HOL中正式确定一个多变量量化取消(QE)算法。我们的算法是完整的,因为它能够将真实算术第一阶逻辑中的任何量化公式减为逻辑等量的无量化公式。我们正式确定的算法是Tarski原QE算法和Ben-Or、Kozen和Reif算法的混合组合,这是在伊莎贝尔/HOL中正式确定的第一个完整的多变量量化量化量化算法。