Linear quantifier elimination as an abstract decision procedure

DOI10.1007/978-3-642-14203-1_27MaRDI QIDQ5747770zbMATH OpenOpenAlexFDO

Authors Nikolaj Bjørner

Publication date 14 September 2010

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-14203-1_27

Mathematics Subject Classification ID

Quantifier elimination, model completeness, and related topics (03C10)

Recommendations

• A Quantifier Elimination Algorithm for Linear Real Arithmetic
• Linear Quantifier Elimination
• Linear quantifier elimination
• Solving quantified linear arithmetic by counterexample-guided instantiation
• Verifying Mixed Real-Integer Quantifier Elimination

Cites work

• (LIA) - Model Evolution with Linear Integer Arithmetic Constraints
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
• A Quantifier Elimination Algorithm for Linear Real Arithmetic
• Applying Linear Quantifier Elimination
• Conflict Resolution
• Effective Quantifier Elimination for Presburger Arithmetic with Infinity
• Enhancing modular OO verification with separation logic
• Generalizing DPLL to Richer Logics
• Integrating Linear Arithmetic into Superposition Calculus
• Linear Quantifier Elimination
• Regression verification for multi-threaded programs
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Superposition modulo linear arithmetic SUP(LA)

Cited in

(17)

• Solving quantified linear arithmetic by counterexample-guided instantiation
• Eliminating message counters in synchronous threshold automata
• A practical approach to model checking duration calculus using Presburger arithmetic
• Refutation-based synthesis in SMT
• A layered algorithm for quantifier elimination from linear modular constraints
• A survey of satisfiability modulo theory
• Quantifier elimination for linear modular constraints
• A simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic
• Virtual substitution for SMT-solving
• Linear Quantifier Elimination
• An approach to multicore parallelism using functional programming: a case study based on Presburger arithmetic
• An effective decision procedure for linear arithmetic over the integers and reals
• Tools and Algorithms for the Construction and Analysis of Systems
• Fast approximations of quantifier elimination
• Cycle encoding-based parameter synthesis for timed automata safety
• Linear quantifier elimination
• Weak quantifier elimination for the full linear theory of the integers

This page was built for publication: Linear quantifier elimination as an abstract decision procedure

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