Thirty years of virtual substitution. Foundations, techniques, applications

DOI10.1145/3208976.3209030MaRDI QIDQ5120170zbMATH OpenOpenAlexWikidataFDO

Authors Thomas Sturm

Publication date 9 September 2020

Published in Proceedings of the 2018 ACM International Symposium on Symbolic and Algebraic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3208976.3209030

zbMATH Keywords

real quantifier eliminationvirtual substitution

Mathematics Subject Classification ID

Quantifier elimination, model completeness, and related topics (03C10) Symbolic computation and algebraic computation (68W30)

Recommendations

• Virtual substitution for SMT-solving
• Towards conflict-driven learning for virtual substitution
• scientific article; zbMATH DE number 1263423
• scientific article; zbMATH DE number 1262432
• Quantifier elimination and cylindrical algebraic decomposition. Proceedings of a symposium, Linz, Austria, October 6--8, 1993

Cited in

(10)

• A logic based approach to finding real singularities of implicit ordinary differential equations
• Algorithmic reduction of biological networks with multiple time scales
• Identifying the parametric occurrence of multiple steady states for some biological networks
• From simplification to a partial theory solver for non-linear real polynomial constraints
• Towards conflict-driven learning for virtual substitution
• Virtual substitution for SMT-solving
• Computing with Tarski formulas and semi-algebraic sets in a web browser
• Verified Quadratic Virtual Substitution for Real Arithmetic
• VIRAS: conflict-driven quantifier elimination for integer-real arithmetic
• Parametric toricity of steady state varieties of reaction networks

Describes a project that uses

Uses Software

• QEPCAD
• REDLOG

This page was built for publication: Thirty years of virtual substitution. Foundations, techniques, applications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5120170)