Virtual Substitution for SMT-Solving

DOI10.1007/978-3-642-22953-4_31zbMath1342.68282OpenAlexW2185350020MaRDI QIDQ3088298

Erika Ábrahám, Florian Corzilius

Publication date: 19 August 2011

Published in: Fundamentals of Computation Theory (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22953-4_31

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (6)

SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving ⋮ Modular strategic SMT solving with \textbf{SMT-RAT} ⋮ Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings ⋮ Virtual Substitution for SMT-Solving ⋮ A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic ⋮ Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)

Uses Software

• QEPCAD
• REDLOG
• z3
• ABsolver

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The complexity of linear problems in fields
• Real quantifier elimination is doubly exponential
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Virtual Substitution for SMT-Solving
• Combined Decision Techniques for the Existential Theory of the Reals
• QEPCAD B
• Linear Quantifier Elimination as an Abstract Decision Procedure

This page was built for publication: Virtual Substitution for SMT-Solving