Fast approximations of quantifier elimination

DOI10.1007/978-3-031-37703-7_4MaRDI QIDQ6535528zbMATHFDO

Authors Isabel García-Contreras, V. K. Hari Govind, Sharon Shoham, Arie Gurfinkel

Publication date 12 January 2024

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Quantifier elimination, model completeness, and related topics (03C10) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• A Quantifier Elimination Algorithm for Linear Real Arithmetic
• New approaches to Boolean quantifier elimination
• Quantifier elimination for linear modular constraints
• Linear quantifier elimination as an abstract decision procedure
• Local quantifier elimination

Cites work

• An abstract domain of uninterpreted functions
• Equality saturation
• Equality saturation: a new approach to optimization
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• SMT-based model checking for recursive programs
• Satisfiability modulo theories
• Simplification by Cooperating Decision Procedures
• Simplify: a theorem prover for program checking
• Verification, Model Checking, and Abstract Interpretation

Cited in

(1)

• “ReLIC: Reduced Logic Inference for Composition” for Quantifier Elimination based Compositional Reasoning

This page was built for publication: Fast approximations of quantifier elimination

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