On the SUP-INF Method for Proving Presburger Formulas

Abstract

This article presents an improved version of Bledsoe's SUP-INF method for proving theorems in a subclass of Presburger arithmetic The improved method is able to determine mvahdRy as well as vahdlty, and provides counterexamples for formulas determined to be mvahd A proof of correctness is given for the algorithms on which the method is based Implementation results are discussed, as is an apphcation to linear programming