Generic Proof Synthesis for Presburger Arithmetic --- Draft

Amine Chaieb and Tobias Nipkow

We develop in complete detail an extension of Cooper's decision procedure for Presburger arithmetic that, in the positive case, returns a proof of the input formula. The algorithm is formulated as a functional program that makes only very minimal assumptions w.r.t. the underlying logical system and is therefore easily adaptable to specific theorem provers.


This technical report has been superseded by this paper.