Thirty Years of Virtual Substitution

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 : 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
Liste complète des métadonnées

https://hal.inria.fr/hal-01889817
Contributor : Thomas Sturm <>
Submitted on : Monday, October 8, 2018 - 9:10:46 AM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM
Document(s) archivé(s) le : Wednesday, January 9, 2019 - 12:59:44 PM

File

p11-sturm.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

20

Files downloads

27