### 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.

### License

BSD License

### Topics

- Computer science/Algorithms/Mathematical

### Related publications

- Kosaian, K., Tan, Y. K., & Platzer, A. (2023). A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs. https://doi.org/10.1145/3573105.3575672

### Session Quantifier_Elimination_Hybrid

- Multiv_Poly_Props
- Multiv_Consistent_Sign_Assignments
- Multiv_Pseudo_Remainder_Sequence
- Hybrid_Multiv_Matrix
- Hybrid_Multiv_Algorithm
- Multiv_Tarski_Query
- Renegar_Modified
- Hybrid_Multiv_Matrix_Proofs
- Hybrid_Multiv_Algorithm_Proofs

### Depends on

- Algebraic Numbers in Isabelle/HOL
- The BKR Decision Procedure for Univariate Real Arithmetic
- Generating linear orders for datatypes
- Descartes' Rule of Signs
- Factorization of Polynomials with Algebraic Coefficients
- Polynomial Interpolation
- Verified Quadratic Virtual Substitution for Real Arithmetic

### Auto-related entries

- Soundness and Completeness of an Axiomatic System for First-Order Logic
- Relational Characterisations of Paths
- A Sequent Calculus for First-Order Logic
- Abstract Soundness
- First-Order Logic According to Fitting

## Cite

×

Quantifier_Elimination_Hybrid-AFP

    @article{Quantifier_Elimination_Hybrid-AFP,
      author  = {Katherine Kosaian and Yong Kiam Tan and André Platzer},
      title   = {A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Quantifier_Elimination_Hybrid.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Jan 12, 2023 : Isabelle2022
- Dec 16, 2022 : Isabelle2022