Thirty Years of Virtual Substitution

Thomas Sturm (1, 2, 3)

1 MPII - Max-Planck-Institut für Informatik
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
3 MOSEL - Proof-oriented development of computer-based systems

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.

Mots clés: Real quantifier elimination; Virtual substitution

Domaines: Calcul formel [cs.SC]

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⟩