Fast approximations of quantifier elimination

DOI10.1007/978-3-031-37703-7_4zbMATH Open1545.68136MaRDI QIDQ6535528FDOQ6535528

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

Publication date: 12 January 2024

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

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)

Cites Work

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

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)