A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
Logic in Computer Science
2022-12-22 v2 Algebraic Geometry
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.
Cite
@article{arxiv.2209.10978,
title = {A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL},
author = {Katherine Kosaian and Yong Kiam Tan and André Platzer},
journal= {arXiv preprint arXiv:2209.10978},
year = {2022}
}
Comments
CPP 2023