Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
From MaRDI portal
Publication:3075472
DOI10.1007/978-3-642-18275-4_8zbMath1318.03045arXiv1011.1036MaRDI 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
Quantifier-free interpolation in combinations of equality interpolating theories, Complete instantiation-based interpolation, Interpolation systems for ground proofs in automated deduction: a survey, Guiding Craig interpolation with domain-specific abstractions, Not all bugs are created equal, but robust reachability can tell the difference, Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations, Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic, Reasoning in the theory of heap: satisfiability and interpolation, 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
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
