KIT | KIT-Bibliothek | Impressum | Datenschutz

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)

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.


Verlagsausgabe §
DOI: 10.5445/IR/1000155892
Veröffentlicht am 15.02.2023
Originalveröffentlichung
DOI: 10.1145/3573105.3575672
Scopus
Zitationen: 2
Dimensions
Zitationen: 1
Cover der Publikation
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 Scopus
Dimensions
Relationen in KITopen
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page