year = "1984", Presburger’s Article on Integer Arithmetic: Remarks and Translation

An early chapter in the development of decision procedures concerns the theory of Presburger arithmetic. The original article presenting the theory was published in German in 1930 under the title “ Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. ” My translation of this article appears here. The translation is preceded by remarks about the historical circumstances surrounding the paper and about the paper itself. The article was written by Moj˙zesz Presburger, a Polish student of mathematics, and presented at a conference in Warsaw in 1929. In it Presburger showed that the part of number theory which uses only the addition function is complete, that is, every formula or its negation is true. This fragment of number theory has come to be known as Presburger arithmetic. Although the motivation of his paper was to prove the theory complete, the method of proof is constructive and yields a decision procedure or algorithm with which every formula of Presburger arithmetic can be determined to be true or false. Probably the earliest theorem-proving program ever written for the computer employed Presburger’s algorithm to prove theorems of Presburger arithmetic. Martin Davis wrote the program in the summer of 1954 for an electronic digital computer with a memory of only 1024 words (Davis 1960). Today algorithms for deciding Presburger arithmetic are important as components of large automatic theorem-proving an