Skip to Main content Skip to Navigation
New interface
Journal articles

A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications

Thomas Sturm 1, 2, 3 
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Abstract : Effective quantifier elimination procedures for first-order theories provide a powerful tool for generically solving a wide range of problems based on logical specifications. In contrast to general first-order provers, quantifier elimination procedures are based on a fixed set of admissible logical symbolswith an implicitly fixed semantics. This admits the use of sub-algorithms from symbolic computation. We are going to focus on quantifier elimination for the reals and its applications giving examples from geometry, verification, and the life sciences. Beyond quantifier elimination we are going to discuss recent results with a subtropical procedure for an existential fragment of the reals. This incomplete decision procedure has been successfully applied to the analysis of reaction systems in chemistry and in the life sciences.
Document type :
Journal articles
Complete list of metadata

Cited literature [75 references]  Display  Hide  Download
Contributor : Thomas Sturm Connect in order to contact the contributor
Submitted on : Thursday, November 30, 2017 - 1:21:51 PM
Last modification on : Friday, July 8, 2022 - 10:06:42 AM
Long-term archiving on: : Thursday, March 1, 2018 - 12:31:00 PM


Explicit agreement for this submission




Thomas Sturm. A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications. Mathematics in Computer Science, 2017, 11 (3-4), pp.483 - 502. ⟨10.1007/s11786-017-0319-z⟩. ⟨hal-01648690⟩



Record views


Files downloads