Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: A First Complete Algorithm for...


view this post on Zulip 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: Mar 28 2024 at 16:17 UTC