Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
From MaRDI portal
Publication:3075472
DOI10.1007/978-3-642-18275-4_8zbMath1318.03045arXiv1011.1036OpenAlexW3138202464MaRDI QIDQ3075472
Angelo Brillout, Philipp Rümmer, Daniel Kroening, Thomas Wahl
Publication date: 15 February 2011
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1011.1036
Related Items (11)
Interpolation systems for ground proofs in automated deduction: a survey ⋮ Not all bugs are created equal, but robust reachability can tell the difference ⋮ Guiding Craig interpolation with domain-specific abstractions ⋮ A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints ⋮ SAT-Based Model Checking ⋮ Interpolation and Model Checking ⋮ Complete instantiation-based interpolation ⋮ Quantifier-free interpolation in combinations of equality interpolating theories ⋮ Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic ⋮ Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations ⋮ Reasoning in the theory of heap: satisfiability and interpolation
Uses Software
Cites Work
- Unnamed Item
- An interpolating theorem prover
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Simplify: a theorem prover for program checking
- Ground Interpolation for the Theory of Equality
- Interpolant Strength
- Presburger arithmetic with unary predicates is Π11 complete
- Automated Deduction – CADE-20
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
- An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
- Verification, Model Checking, and Abstract Interpretation
- Tools and Algorithms for the Construction and Analysis of Systems
This page was built for publication: Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
