VIRAS: conflict-driven quantifier elimination for integer-real arithmetic

DOI10.29007/KG4VMaRDI QIDQ7025191zbMATH OpenFDO

Authors Johannes Schoisswohl, Laura Kovács, Konstantin Korovin

Publication date 19 February 2025

zbMATH Keywords

SMTarithmeticdecision procedurequantifier eliminationvirtual substitutionLIRA

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) First-order arithmetic and fragments (03F30) Quantifier elimination, model completeness, and related topics (03C10)

Cites work

• scientific article; zbMATH DE number 1302474 (Why is no real title available?)
• scientific article; zbMATH DE number 3408928 (Why is no real title available?)
• A CDCL-style calculus for solving non-linear constraints
• Applying Linear Quantifier Elimination
• Conflict Resolution
• Cutting to the chase.
• Cylindrical Algebraic Decomposition I: The Basic Algorithm
• Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
• Seventeen provers under the hammer
• Solving quantified linear arithmetic by counterexample-guided instantiation
• Solving systems of linear inequalities by bound propagation
• Thirty years of virtual substitution. Foundations, techniques, applications
• Towards conflict-driven learning for virtual substitution

Cited in

(1)

• Ground truth: checking \textsc{Vampire} proofs via satisfiability modulo theories

This page was built for publication: VIRAS: conflict-driven quantifier elimination for integer-real arithmetic

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