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

Thomas Sturm 1, 2
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
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 metadatas

Cited literature [75 references]  Display  Hide  Download

https://hal.inria.fr/hal-01648690
Contributor : Thomas Sturm <>
Submitted on : Thursday, November 30, 2017 - 1:21:51 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:04 PM
Long-term archiving on : Thursday, March 1, 2018 - 12:31:00 PM

File

10.1007_s11786-017-0319-z.pdf
Explicit agreement for this submission

Identifiers

Collections

Citation

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

Share

Metrics

Record views

161

Files downloads

129