2017/04/26 by Thomas Sturm · 2 citations
Computer Science · Mathematics · #Advanced Database Systems and Queries #Algorithm #Artificial intelligence #Automated reasoning #Automated theorem proving #Computer science #Contrast (vision) #Focus (optics) #Formal Methods in Verification #Fragment (logic) #Logic, programming, and type systems #Mathematics #Programming language #Quantifier (linguistics) #Quantifier elimination #Satisfiability #Semantics (computer science) #Set (abstract data type) #Theoretical computer science
paper · pdf · doi:10.1007/s11786-017-0319-z
openalex publication_date 2017/04/26 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/31
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 symbols with 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.