Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Verified Quadratic Virtual Sub...


view this post on Zulip 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: Jul 15 2022 at 23:21 UTC