An interpolating sequent calculus for quantifier-free Presburger arithmetic
DOI10.1007/S10817-011-9237-YzbMATH Open1259.03043OpenAlexW2071365289MaRDI QIDQ438556FDOQ438556
Authors: Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl 
Publication date: 31 July 2012
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-011-9237-y
Recommendations
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- Interpolating quantifier-free Presburger arithmetic
- Beyond quantifier-free interpolation in extensions of Presburger arithmetic
- Interpolant based decision procedure for quantifier-free Presburger arithmetic
- Tools and Algorithms for the Construction and Analysis of Systems
Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Structure of proofs (03F07) First-order arithmetic and fragments (03F30) Interpolation, preservation, definability (03C40)
Cites Work
- Title not available (Why is that?)
- An interpolating theorem prover
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Interpolants for Linear Arithmetic in SMT
- Polynomial Algorithms for Computing the Smith and Hermite Normal Forms of an Integer Matrix
- Title not available (Why is that?)
- Constraint Solving for Interpolation
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- Lazy Abstraction with Interpolants
- A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
- Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
- Interpolating quantifier-free Presburger arithmetic
- Interpolant Generation for UTVPI
- Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
Cited In (11)
- Reasoning in the theory of heap: satisfiability and interpolation
- Preface: Special issue on interpolation
- Parallelizing SMT solving: lazy decomposition and conciliation
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- On recursion-free Horn clauses and Craig interpolation
- Complete instantiation-based interpolation
- Interpolating quantifier-free Presburger arithmetic
- Beyond quantifier-free interpolation in extensions of Presburger arithmetic
- Craig interpolation with clausal first-order tableaux
- Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
- Interpolant based decision procedure for quantifier-free Presburger arithmetic
Uses Software
This page was built for publication: An interpolating sequent calculus for quantifier-free Presburger arithmetic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q438556)
