Generic Proof Synthesis for Presburger Arithmetic --- Draft
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