An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic

Craig interpolation has become a versatile tool in formal verification, for instance to generate intermediate assertions for safety analysis of programs. Interpolants are typically determined by annotating the steps of an unsatisfiability proof with partial interpolants. In this paper, we consider Craig interpolation for full quantifier-free Presburger arithmetic (QFPA), for which currently no efficient interpolation procedures are known. Closing this gap, we introduce an interpolating sequent calculus for QFPA and prove it to be sound and complete. We have extended the Princess theorem prover to generate interpolating proofs, and applied it to a large number of publicly available linear integer arithmetic benchmarks. The results indicate the robustness and efficiency of our proof-based interpolation procedure.

• Type: Conference
• Year: 2010
• Where: CADE
• Authors: Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl
• Keywords: CADE 2010, Craig Interpolation, Efficient Interpolation Procedures, Interpolation Procedure, Logical Reasoning