---
title: "A New Mehtod for Proving Certain Presburger Formules"
authors:
  - "W. W. Bledsoe"
doi: ""
url: "https://ijcai.org/proceedings/1975/3"
pdf: "https://ijcai.org/proceedings/1975/0003.pdf"
venue: "Proceedings of the Fourth International Joint Conference on Artificial Intelligence"
year: 1975
pages: "15-20"
track: "Mathematical and Theoretical Aspects of A.I"
keywords:
---

# A New Mehtod for Proving Certain Presburger Formules

W. W. Bledsoe

*Proceedings of the Fourth International Joint Conference on Artificial Intelligence*, pages 15-20.

## Abstract

This paper describes a new method for determining the validity of certain formulas from Presburger Arithmetic, namely those with only universally quantified variables. To do this the notion of a Presburger formula, is generalized slightly to that of a quasi-linear formula. This so called "sup-inf'' method seems particularly suited for proving certain verification conditions that arise from program validation, especially those in which "proof by cases" is required. It also eliminates the need for proof by enumeration, inherent in some methods described earlier in the literature, which sometimes require a search through a large number of consecutive integers. These algorithms have been programmed and used extensively as a part of an automatic theorem proving system.