Linear Quantifier Elimination as an Abstract Decision Procedure

DOI10.1007/978-3-642-14203-1_27zbMath1291.68325OpenAlexW1506481780MaRDI QIDQ5747770

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

Related Items (8)

A layered algorithm for quantifier elimination from linear modular constraints ⋮ Solving quantified linear arithmetic by counterexample-guided instantiation ⋮ An approach to multicore parallelism using functional programming: a case study based on Presburger arithmetic ⋮ Eliminating message counters in synchronous threshold automata ⋮ A practical approach to model checking duration calculus using Presburger arithmetic ⋮ Refutation-based synthesis in SMT ⋮ Virtual Substitution for SMT-Solving ⋮ A Survey of Satisfiability Modulo Theory

Cites Work

• Regression Verification for Multi-threaded Programs
• Applying Linear Quantifier Elimination
• Conflict Resolution
• Enhancing modular OO verification with separation logic
• Solving SAT and SAT Modulo Theories
• Linear Quantifier Elimination
• Integrating Linear Arithmetic into Superposition Calculus
• Generalizing DPLL to Richer Logics
• Effective Quantifier Elimination for Presburger Arithmetic with Infinity
• Superposition Modulo Linear Arithmetic SUP(LA)
• A Quantifier Elimination Algorithm for Linear Real Arithmetic
• (LIA) - Model Evolution with Linear Integer Arithmetic Constraints
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic

This page was built for publication: Linear Quantifier Elimination as an Abstract Decision Procedure