An interpolating sequent calculus for quantifier-free Presburger arithmetic

DOI10.1007/s10817-011-9237-yzbMath1259.03043OpenAlexW2071365289MaRDI QIDQ438556

Philipp Rümmer, Angelo Brillout, Daniel Kroening, 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

zbMATH Keywords

sequent calculusCraig interpolationPresburger arithmetic

Mathematics Subject Classification ID

Related Items (7)

Preface: Special issue on interpolation ⋮ Craig interpolation with clausal first-order tableaux ⋮ Complete instantiation-based interpolation ⋮ Parallelizing SMT solving: lazy decomposition and conciliation ⋮ On recursion-free Horn clauses and Craig interpolation ⋮ Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic ⋮ Reasoning in the theory of heap: satisfiability and interpolation

Uses Software

• Princess
• OpenSMT
• CSIsat
• FOCI

Cites Work

• Unnamed Item
• Unnamed Item
• An interpolating theorem prover
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
• Interpolants for Linear Arithmetic in SMT
• Polynomial Algorithms for Computing the Smith and Hermite Normal Forms of an Integer Matrix
• Interpolating Quantifier-Free Presburger Arithmetic
• Interpolant Generation for UTVPI
• Constraint Solving for Interpolation
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
• An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
• Lazy Abstraction with Interpolants
• Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic

This page was built for publication: An interpolating sequent calculus for quantifier-free Presburger arithmetic