Fast approximations of quantifier elimination

DOI10.1007/978-3-031-37703-7_4MaRDI QIDQ6535528zbMATH OpenFDO

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

Publication date 12 January 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-37703-7_4

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
• Satisfiability modulo theories
• Simplification by Cooperating Decision Procedures
• Simplify: a theorem prover for program checking
• SMT-based model checking for recursive programs
• Verification, Model Checking, and Abstract Interpretation

Cited in

(5)

• “ReLIC: Reduced Logic Inference for Composition” for Quantifier Elimination based Compositional Reasoning
• Relatively complete and efficient partial quantifier elimination
• Inner and outer approximations of arbitrarily quantified reachability problems
• SAT solving for variants of first-order subsumption
• Inner and outer approximate quantifier elimination for general reachability problems

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)