Virtual substitution for SMT-solving

DOI10.1007/978-3-642-22953-4_31MaRDI QIDQ3088298zbMATH OpenOpenAlexFDO

Authors Florian Corzilius, Erika Ábrahám

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

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

Recommendations

• Towards conflict-driven learning for virtual substitution
• Thirty years of virtual substitution. Foundations, techniques, applications
• I-RiSC: an SMT-compliant solver for the existential fragment of real algebra
• Satisfiability modulo theories
• On Gröbner bases in the context of satisfiability-modulo-theories solving over the real numbers

Cites work

• Combined Decision Techniques for the Existential Theory of the Reals
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• scientific article; zbMATH DE number 1302474 (Why is no real title available?)
• scientific article; zbMATH DE number 1157666 (Why is no real title available?)
• scientific article; zbMATH DE number 5263038 (Why is no real title available?)
• scientific article; zbMATH DE number 3053259 (Why is no real title available?)
• Linear quantifier elimination as an abstract decision procedure
• QEPCAD B
• Real quantifier elimination is doubly exponential
• The complexity of linear problems in fields
• Virtual substitution for SMT-solving

Cited in

(12)

• Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
• Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
• Modular strategic SMT solving with \textbf{SMT-RAT}
• A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
• On Gröbner bases in the context of satisfiability-modulo-theories solving over the real numbers
• Towards conflict-driven learning for virtual substitution
• I-RiSC: an SMT-compliant solver for the existential fragment of real algebra
• Virtual substitution for SMT-solving
• \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
• Thirty years of virtual substitution. Foundations, techniques, applications
• FMplex: a novel method for solving linear real arithmetic problems
• FMplex: exploring a bridge between Fourier-Motzkin and simplex

Describes a project that uses

Uses Software

• QEPCAD
• REDLOG
• z3
• ABsolver

This page was built for publication: Virtual substitution for SMT-solving

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