Email Gateway (Dec 16 2022 at 14:48): Email Gateway (Dec 16 2022 at 14:48):From: Tobias Nipkow <nipkow@in.tum.de>
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
Katherine Cordwell, Yong Kiam Tan and André Platzer
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.
https://www.isa-afp.org/entries/Quantifier_Elimination_Hybrid.html
Enjoy!
smime.p7s
Last updated: Jan 04 2025 at 20:18 UTC