Conference proceeding
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp.211-224
ACM Conferences
CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs
01/11/2023
DOI: 10.1145/3573105.3575672
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.
Details
- Title: Subtitle
- A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
- Creators
- Katherine Kosaian - Carnegie Mellon University, USAYong Kiam Tan - Carnegie Mellon UniversityAndré Platzer - KIT, Germany
- Resource Type
- Conference proceeding
- Publication Details
- Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp.211-224
- Conference
- CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs
- Series
- ACM Conferences
- DOI
- 10.1145/3573105.3575672
- Publisher
- ACM
- Language
- English
- Date published
- 01/11/2023
- Academic Unit
- Computer Science
- Record Identifier
- 9984696722702771
Metrics
19 Record Views