  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.
