Skip to Main content Skip to Navigation
Conference papers

Thirty Years of Virtual Substitution

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 : In 1988, Weispfenning published a seminal paper introducing a substitution technique for quantifier elimination in the linear theories of ordered and valued fields. The original focus was on complexity bounds including the important result that the decision problem for Tarski Algebra is bounded from below by a double exponential function. Soon after, Weispfenning's group began to implement substitution techniques in software in order to study their potential applicability to real world problems. Today virtual substitution has become an established computational tool, which greatly complements cylindrical algebraic decomposition. There are powerful implementations and applications with a current focus on satisfia-bility modulo theory solving and qualitative analysis of biological networks.
Document type :
Conference papers
Complete list of metadata

Cited literature [72 references]  Display  Hide  Download
Contributor : Thomas Sturm Connect in order to contact the contributor
Submitted on : Monday, October 8, 2018 - 9:10:46 AM
Last modification on : Wednesday, November 3, 2021 - 7:09:21 AM
Long-term archiving on: : Wednesday, January 9, 2019 - 12:59:44 PM


Files produced by the author(s)




Thomas Sturm. Thirty Years of Virtual Substitution. ISSAC 2018 - 43rd International Symposium on Symbolic and Algebraic Computation, Jul 2018, New York, United States. ⟨10.1145/3208976.3209030⟩. ⟨hal-01889817⟩



Les métriques sont temporairement indisponibles