Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl. An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. Journal of Automated Reasoning, 47(4):341-367, 2011. [doi]
@article{BrilloutKRW11-0, title = {An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic}, author = {Angelo Brillout and Daniel Kroening and Philipp Rümmer and Thomas Wahl}, year = {2011}, doi = {10.1007/s10817-011-9237-y}, url = {http://dx.doi.org/10.1007/s10817-011-9237-y}, researchr = {https://researchr.org/publication/BrilloutKRW11-0}, cites = {0}, citedby = {0}, journal = {Journal of Automated Reasoning}, volume = {47}, number = {4}, pages = {341-367}, }