An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.

Angelo Brillout, Daniel Kroening, Philipp Rmmer, Thomas Wahl

Browse the full CADE paper archive.