Thirty Years of Virtual Substitution - Archive ouverte HAL Access content directly
Conference Papers Year : 2018

Thirty Years of Virtual Substitution


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.
Fichier principal
Vignette du fichier
p11-sturm.pdf (1.19 Mo) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-01889817 , version 1 (08-10-2018)



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⟩
35 View
246 Download



Gmail Facebook Twitter LinkedIn More