Email Gateway (Oct 19 2021 at 13:44): Email Gateway (Oct 19 2021 at 13:44):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
I’m happy to announce a new quantifier elimination procedure in the AFP.
Verified Quadratic Virtual Substitution for Real Arithmetic
by Matias Scharager, Katherine Cordwell, Stefan Mitsch and André Platzer
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. Our framework is modularized and easily expandable
(to facilitate integrating future optimizations), and could serve as a basis for
developing practical general-purpose QE algorithms. 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, Wolfram Engine, and SMT-RAT. This identified
inconsistencies in some tools, underscoring the significance of a verified
approach for the intricacies of real arithmetic.
https://www.isa-afp.org/entries/Virtual_Substitution.html
Enjoy,
René
Last updated: Jan 04 2025 at 20:18 UTC