Thirty Years of Virtual Substitution

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.
Type de document :
Communication dans un congrès
ISSAC 2018 - 43rd International Symposium on Symbolic and Algebraic Computation, Jul 2018, New York, United States. 18, 2018, 〈10.1145/3208976.3209030〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01889817
Contributeur : Thomas Sturm <>
Soumis le : lundi 8 octobre 2018 - 09:10:46
Dernière modification le : mercredi 24 octobre 2018 - 16:09:15

Fichier

p11-sturm.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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. 18, 2018, 〈10.1145/3208976.3209030〉. 〈hal-01889817〉

Partager

Métriques

Consultations de la notice

9

Téléchargements de fichiers

12