A Decision Procedure for Presburger Arithmetic with Functions and Equality

Abstract

Many of the formulas one tends to encounter in program verification are contained in the quantifier-free Presburger Arithmetic and its extension by predicate and function symbols. Remarkable work for both the unextended and the extended class has been done by Robert Shostak. Particularly for the quantifier-free Presburger Arithmetic, he developed a very elegant algorithm based on the computation of loop residues in a graph. The algorithm decides the satisfiability of of a conjunction of atomic formulas of this theory. This diploma thesis presents the development of a decision procedure for the satisfiability of a conjunction of atomic formulas of the quantifier-free Presburger Arithmetic extended by predicate and function symbols: The EQUALITY_LOOP_RESIDUE procedure. This procedure combines both the concept of the LOOP_RESIDUE method in a refined version adjusted to the specific problems of the extended class and the concept of rewriting. The connection of this decision problem to ground terms is pointed out and a polynomial time algorithm for computing a canonical rewriting system equivalent to a finite set of ground equations recently (1988) presented by Gallier, Narendran, Plaisted, Raatz, and Snyder can be used as subprocedure in the newly developed decision procedure. The EQUALITY_LOOP_RESIDUE procedure does not only improve the decision process of the satisfiability of a conjunction of atomic formulas, but also the determination of the validity of a quantifier-free Presburger formula including predicate and function symbols.