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.
pdf
This technical report has been superseded by this
paper.