A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
Kosaian, Katherine; Tan, Yong Kiam; Platzer, André
1
1 Institut für Informationssicherheit und Verlässlichkeit (KASTEL), Karlsruher Institut für Technologie (KIT)
11 Institut für Informationssicherheit und Verlässlichkeit (KASTEL), Karlsruher Institut für Technologie (KIT)
Abstract:
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.
| Zugehörige Institution(en) am KIT | Institut für Informationssicherheit und Verlässlichkeit (KASTEL) |
| Publikationstyp | Proceedingsbeitrag |
| Publikationsdatum | 11.01.2023 |
| Sprache | Englisch |
| Identifikator | ISBN: 979-84-00-70026-2 KITopen-ID: 1000155892 |
| HGF-Programm | 46.23.01 (POF IV, LK 01) Methods for Engineering Secure Systems |
| Erschienen in | Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs |
| Veranstaltung | 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (2023), Boston, MA, USA, 16.01.2023 – 17.01.2023 |
| Verlag | Association for Computing Machinery (ACM) |
| Seiten | 211–224 |
| Schlagwörter | quantifier elimination, theorem proving, real arithmetic, multivariate polynomials |
| Nachgewiesen in | Dimensions Scopus |
| Relationen in KITopen |