diff --git a/metadata/entries/Quantifier_Elimination_Hybrid.toml b/metadata/entries/Quantifier_Elimination_Hybrid.toml --- a/metadata/entries/Quantifier_Elimination_Hybrid.toml +++ b/metadata/entries/Quantifier_Elimination_Hybrid.toml @@ -1,36 +1,36 @@ title = "A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL" date = 2022-12-15 topics = [ "Computer science/Algorithms/Mathematical", ] 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" note = "" [authors] [authors.cordwell] email = "cordwell_email" [authors.tan] email = "tan_email" [authors.platzer] email = "platzer_email" [contributors] [notify] cordwell = "cordwell_email" tan = "tan_email" platzer = "platzer_email" [history] [extra] [related] dois = [ - "10.48550/arXiv.2209.10978", + "10.1145/3573105.3575672", ] pubs = [] diff --git a/web/entries/Quantifier_Elimination_Hybrid.html b/web/entries/Quantifier_Elimination_Hybrid.html --- a/web/entries/Quantifier_Elimination_Hybrid.html +++ b/web/entries/Quantifier_Elimination_Hybrid.html @@ -1,187 +1,188 @@ A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL - Archive of Formal Proofs

A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL

Katherine Cordwell 📧, Yong Kiam Tan 📧 and André Platzer 📧

December 15, 2022

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

Related publications

  • - Kosaian, K., Tan, Y. K., & Platzer, A. (2022). A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. ArXiv. https://doi.org/10.48550/ARXIV.2209.10978 + 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

Depends on

Auto-related entries

Cite

× 
@article{Quantifier_Elimination_Hybrid-AFP,
   author  = {Katherine Cordwell 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
\ No newline at end of file