Katherine Cordwell: Formalizing Algorithms for Real Quantifier Elimination

Real arithmetic questions involving the “there exists” and “for all” quantifiers arise in various fields, including formalized mathematics, rigorous engineering domains, and life sciences. Although Tarski proved that real quantified statements can always be reduced to logically equivalent quantifier-free statements through quantifier elimination (QE), QE algorithms are notoriously complicated. This makes QE algorithms difficult to formally verify---formally verified algorithms require accompanying proofs of correctness (typically developed in theorem provers) that rely only on a set of trusted logical axioms---and so in practice, QE problems must be solved with unverified software. This is undesirable given the subtlety of QE algorithms and the safety-critical nature of their applications. In recent work, my collaborators and I found that some of the existing unverified QE tools are self-contradictory on (in total) 137 benchmarks, which underscores the need for more support for practical formally verified QE.

My proposed approach is twofold: First, verify a general-purpose multivariate quantifier elimination algorithm based on the Ben-Or, Kozen, and Reif (BKR) algorithm and its variant by Renegar---to fit in a potential “sweet spot” in between practicality of use and ease of verification. Second, augment BKR with strong additional methods and preprocessing methods, including virtual substitution (an extremely practical QE method for QE problems that involve low-degree polynomials). This talk discusses progress towards this ambitious goal, which includes verifying, in the theorem prover Isabelle/HOL, linear and quadratic virtual substitution, univariate BKR, and a naive multivariate quantifier elimination algorithm that can serve as a stepping-stone to multivariate BKR (in joint work).