A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL

TL;DR

This paper formalizes a complete multivariate quantifier elimination algorithm within Isabelle/HOL, combining Tarski's and Ben-Or, Kozen, and Reif's methods, enabling reduction of any first-order real arithmetic formula to an equivalent quantifier-free form.

Contribution

It presents the first formalization of a complete multivariate QE algorithm in Isabelle/HOL, integrating two classical approaches.

Findings

Successfully formalized a complete multivariate QE algorithm in Isabelle/HOL

Demonstrated the algorithm's ability to reduce any first-order real arithmetic formula

Bridged classical QE methods within a formal proof assistant environment

Abstract

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.