Editing Presburger arithmetic

{{Short description|Decidable first-order theory of the natural numbers with addition}}
'''Presburger arithmetic''' is the [[first-order predicate calculus|first-order theory]] of the [[natural number]]s with [[addition]], named in honor of [[Mojżesz Presburger]], who introduced it in 1929. The [[signature (mathematical logic)|signature]] of Presburger arithmetic contains only the addition operation and [[equality (mathematics)|equality]], omitting the [[multiplication]] operation entirely. The theory is [[Computable set|computably]] axiomatizable; the axioms include a schema of [[mathematical induction|induction]].

Presburger arithmetic is much weaker than [[Peano arithmetic]], which includes both addition and multiplication operations. Unlike Peano arithmetic, Presburger arithmetic is a [[Decidability (logic)|decidable theory]]. This means it is possible to algorithmically determine, for any sentence in the language of Presburger arithmetic, whether that sentence is provable from the axioms of Presburger arithmetic. The asymptotic running-time [[Analysis of algorithms|computational complexity]] of this algorithm is at least [[Double exponential function|doubly exponential]], however, as shown by {{harvtxt|Fischer|Rabin|1974}}.

==Overview==
The language of Presburger arithmetic contains constants 0 and 1 and a binary function +, interpreted as addition.

In this language, the axioms of Presburger arithmetic are the [[universal closure]]s of the following:
# ¬(0 = ''x'' + 1)
# ''x'' + 1 = ''y'' + 1 → ''x'' = ''y''
# ''x'' + 0 = ''x''
# ''x'' + (''y'' + 1) = (''x'' + ''y'') + 1
# Let ''P''(''x'') be a [[first-order logic|first-order formula]] in the language of Presburger arithmetic with a  free variable ''x'' (and possibly other free variables). Then the following formula is an axiom:{{pb}}(''P''(0) &and; ∀''x''(''P''(''x'') → ''P''(''x'' + 1))) → ∀''y'' ''P''(''y'').

(5) is an [[axiom schema]] of [[Mathematical Induction|induction]], representing infinitely many axioms. These cannot be replaced by any finite number of axioms, that is, Presburger arithmetic is not finitely axiomatizable in first-order logic.{{sfn|Zoethout|2015|p=8|loc=Theorem 1.2.4.}}

Presburger arithmetic can be viewed as a [[First-order logic#First-order theories, models, and elementary classes|first-order theory]] with equality containing precisely all consequences of the above axioms. Alternatively, it can be defined as the set of those sentences that are true in the [[Interpretation (logic)#Intended interpretations|intended interpretation]]: the structure of non-negative integers with constants 0, 1, and the addition of non-negative integers.

Presburger arithmetic is designed to be complete and decidable. Therefore, it cannot formalize concepts such as [[divisibility]] or [[primality]], or, more generally, any number concept leading to multiplication of variables. However, it can formulate individual instances of divisibility; for example, it proves "for all ''x'', there exists ''y'' : (''y'' + ''y'' = ''x'') ∨ (''y'' + ''y'' + 1 = ''x'')". This states that every number is either even or odd.

==Properties==

{{harvtxt|Presburger|1929}} proved Presburger arithmetic to be:
* [[Consistency proof|consistent]]: There is no statement in Presburger arithmetic that can be deduced from the axioms such that its negation can also be deduced.
* [[Completeness (logic)|complete]]: For each statement in the language of Presburger arithmetic, either it is possible to deduce it from the axioms or it is possible to deduce its negation. 
* [[Decidability (logic)|decidable]]: There exists an [[algorithm]] that decides whether any given statement in Presburger arithmetic is a theorem or a nontheorem - note that a "nontheorem" is a formula that cannot be proved, not in general necessarily one whose negation can be proved, but in the case of a complete theory like here both definitions are equivalent.

The decidability of Presburger arithmetic can be shown using [[quantifier elimination]], supplemented by reasoning about [[Modular arithmetic|arithmetical congruence]].{{sfn|Presburger|1929}}{{sfn|Büchi|1962}}{{sfn|Monk|2012|p=240}}{{sfn|Nipkow|2010}}{{sfn|Enderton|2001|p=188}} The steps used to justify a quantifier elimination algorithm can be used to define computable axiomatizations that do not necessarily contain the axiom schema of induction.{{sfn|Presburger|1929}}{{sfn|Stansifer|1984}}

In contrast, [[Peano arithmetic]], which is Presburger arithmetic augmented with multiplication, is not decidable, as proved by Church alongside the negative answer to the [[Entscheidungsproblem]]. By [[Gödel's incompleteness theorem]], Peano arithmetic is incomplete and its consistency is not internally provable (but see [[Gentzen's consistency proof]]).

=== Computational complexity ===
The decision problem for Presburger arithmetic is an interesting example in [[computational complexity theory]] and [[computation]]. Let ''n'' be the length of a statement in Presburger arithmetic. Then {{harvtxt|Fischer|Rabin|1974}} proved that, in the worst case, the proof of the statement in first-order logic has length at least <math>2^{2^{cn}}</math>, for some constant ''c''>0. Hence, their decision algorithm for Presburger arithmetic has runtime at least exponential. Fischer and Rabin also proved that for any reasonable axiomatization (defined precisely in their paper), there exist theorems of length ''n'' that have [[double exponential function|doubly exponential]] length proofs. Fischer and Rabin's work also implies that Presburger arithmetic can be used to define formulas that correctly calculate any algorithm as long as the inputs are less than relatively large bounds. The bounds can be increased, but only by using new formulas. On the other hand, a triply exponential upper bound on a decision procedure for Presburger arithmetic was proved by {{harvtxt|Oppen|1978}}.

A more tight complexity bound was shown using alternating complexity classes by {{harvtxt|Berman|1980}}. The set of true statements in Presburger arithmetic (PA) is shown complete for [[Alternating Turing machine|TimeAlternations]](2<sup>2<sup>n<sup>O(1)</sup></sup></sup>, n). Thus, its complexity is between double exponential nondeterministic time (2-NEXP) and double exponential space (2-EXPSPACE). Completeness is under [[Karp reduction]]s. (Also, note that while Presburger arithmetic is commonly abbreviated PA, in mathematics in general PA usually means [[Peano arithmetic]].)

For a more fine-grained result, let PA(i) be the set of true Σ<sub>i</sub> PA statements, and PA(i, j) the set of true Σ<sub>i</sub> PA statements with each quantifier block limited to j variables.  '<' is considered to be quantifier-free; here, bounded quantifiers are counted as quantifiers.<br/>
PA(1, j) is in P, while PA(1) is NP-complete.{{sfn|Nguyen Luu|2018|loc=chapter 3}}<br/>
For i > 0 and j > 2, PA(i + 1, j) is [[Polynomial_hierarchy|Σ<sub>i</sub><sup>P</sup>-complete]]. The hardness result only needs j>2 (as opposed to j=1) in the last quantifier block.<br/>
For i>0, PA(i+1) is [[Exponential_hierarchy|Σ<sub>i</sub><sup>EXP</sup>-complete]].{{sfn|Haase|2014|pp=47:1-47:10}}

Short <math>\Sigma_n</math> Presburger Arithmetic (<math>n>2</math>) is <math>\Sigma_{n-2}^P</math> complete (and thus NP complete for <math>n=3</math>).  Here, 'short' requires bounded (i.e. <math>O(1)</math>) sentence size except that integer constants are unbounded (but their number of bits in binary counts against input size).  Also, <math>\Sigma_2</math> two variable PA (without the restriction of being 'short') is NP-complete.{{sfn|Nguyen|Pak|2017}} Short <math>\Pi_2</math> (and thus <math>\Sigma_2</math>) PA is in P, and this extends to fixed-dimensional parametric integer linear programming.{{sfn|Eisenbrand|Shmonin|2008}}

==Applications==
Because Presburger arithmetic is decidable, [[automatic theorem prover]]s for Presburger arithmetic exist. For example, the [[Coq (software)|Coq]] and [[Lean (proof assistant)|Lean]] proof assistant systems feature the tactic ''omega'' for Presburger arithmetic and the [[Isabelle (proof assistant)|Isabelle proof assistant]] contains a verified quantifier elimination procedure by {{harvtxt|Nipkow|2010}}. The double exponential complexity of the theory makes it infeasible to use the theorem provers on complicated formulas, but this behavior occurs only in the presence of nested quantifiers: {{harvtxt|Nelson|Oppen|1978}} describe an automatic theorem prover that uses the [[simplex algorithm]] on an extended Presburger arithmetic without nested quantifiers to prove some of the instances of quantifier-free Presburger arithmetic formulas. More recent [[satisfiability modulo theories]] solvers use complete [[integer programming]] techniques to handle quantifier-free fragment of Presburger arithmetic theory.{{sfn|King|Barrett|Tinelli|2014}}

Presburger arithmetic can be extended to include multiplication by constants, since multiplication is repeated addition. Most array subscript calculations then fall within the region of decidable problems.<ref>For example, in the [[C (programming language)|C programming language]], if <code>a</code> is an array of 4 bytes element size, the expression <code>a[i]</code> can be translated to <code>a<sub>baseadr</sub>+i+i+i+i</code>, which fits the restrictions of Presburger arithmetic.</ref> This approach is the basis of at least five{{cn|date=October 2024}} proof-of-[[Correctness (computer science)|correctness]] systems for [[computer programs]], beginning with the [[Stanford Pascal Verifier]] in the late 1970s and continuing through to Microsoft's Spec# system of 2005.

==Presburger-definable integer relation==
Some properties are now given about integer [[Finitary relation|relations]] definable in Presburger Arithmetic. For the sake of simplicity, all relations considered in this section are over non-negative integers.

A relation is  Presburger-definable if and only if it is a [[semilinear set]].{{sfn|Ginsburg|Spanier|1966|pp=285–296}}

A unary integer relation <math>R</math>, that is, a set of non-negative integers, is Presburger-definable if and only if it is ultimately periodic. That is, if there exists a threshold <math>t\in \N</math> and a positive period <math>p\in\N^{>0}</math> such that, for all integer <math>n</math> such that <math>|n|\ge t</math>, <math>n\in R</math> if and only if <math>n+p\in R</math>.

By the [[Cobham–Semenov theorem]], a relation is Presburger-definable if and only if it is definable in [[Büchi arithmetic]] of base <math>k</math> for all <math>k\ge2</math>.{{sfn|Cobham|1969|pp=186–192}}{{sfn|Semenov|1977|pp=403–418}} A relation definable in Büchi arithmetic of base <math>k</math> and <math>k'</math> for <math>k</math> and <math>k'</math> being [[Multiplicative independence|multiplicatively independent]] integers is Presburger definable.

An integer relation <math>R</math> is Presburger-definable if and only if all sets of integers that are definable in first-order logic with addition and <math>R</math> (that is, Presburger arithmetic plus a predicate for <math>R</math>) are Presburger-definable.{{sfn|Michaux|Villemaire|1996|pp=251–277}} Equivalently, for each relation <math>R</math> that is not Presburger-definable, there exists a first-order formula with addition and <math>R</math> that defines a set of integers that is not definable using only addition.

===Muchnik's characterization===
Presburger-definable relations admit another characterization: by Muchnik's theorem.{{sfn|Muchnik|2003|pp=1433–1444}} It is more complicated to state, but led to the proof of the two former characterizations. Before Muchnik's theorem can be stated, some additional definitions must be introduced.

Let <math>R\subseteq\N^d</math> be a set, the section <math>x_i = j</math> of <math>R</math>, for <math>i < d</math> and <math>j \in \N</math> is defined as 
:<math>\left \{(x_0,\ldots,x_{i-1},x_{i+1},\ldots,x_{d-1})\in\N^{d-1}\mid(x_0,\ldots,x_{i-1},j,x_{i+1},\ldots,x_{d-1})\in R \right \}.</math>

Given two sets <math>R,S\subseteq\N^d</math> and a {{nowrap|<math>d</math>-tuple}} of integers <math>(p_0,\ldots,p_{d-1})\in\N^d</math>, the set <math>R</math> is called <math>(p_0,\dots,p_{d-1})</math>-periodic in <math>S</math> if, for all <math>(x_0, \dots, x_{d-1}) \in S</math> such that <math>(x_0+p_0,\dots,x_{d-1}+p_{d-1})\in S,</math> then <math>(x_0,\ldots,x_{d-1})\in R</math> if and only if <math>(x_0+p_0,\dots,x_{d-1}+p_{d-1})\in R</math>. For <math>s\in\N</math>, the set  <math>R</math> is said to be {{nowrap|<math>s</math>-periodic}} in <math>S</math> if it is {{nowrap|<math>(p_0,\ldots,p_{d-1})</math>-periodic}} for some <math>(p_0,\dots,p_{d-1})\in\Z^d</math> such that  

:<math>\sum_{i=0}^{d-1}|p_i| < s.</math>

Finally, for <math>k,x_0,\dots,x_{d-1}\in\N</math> let 
:<math>C(k,(x_0,\ldots,x_{d-1}))= \left \{(x_0+c_0,\dots,x_{d-1}+c_{d-1})\mid 0 \leq c_i < k \right \}</math> 
denote the cube of size <math>k</math> whose lesser corner is <math>(x_0,\dots,x_{d-1})</math>.

{{math theorem|name=Muchnik's Theorem|math_statement= <math>R\subseteq\N^d</math> is Presburger-definable if and only if:
* if <math>d > 1</math> then  all sections of <math>R</math> are Presburger-definable and 
* there exists <math>s\in\N</math> such that, for every <math>k\in\N</math>, there exists <math>t\in\N</math> such that for all <math>(x_0,\dots,x_{d-1})\in\N^d</math> with <math display="block">\sum_{i=0}^{d-1}x_i>t,</math> <math>R</math> is {{nowrap|<math>s</math>-periodic}} in <math>C(k,(x_0,\dots,x_{d-1}))</math>.}}

Intuitively, the integer <math>s</math> represents the length of a shift, the integer <math>k</math> is the size of the cubes and <math>t</math> is the threshold before the periodicity. This result remains true when the condition 

:<math>\sum_{i=0}^{d-1}x_i>t</math> 

is replaced either by <math>\min(x_0,\ldots,x_{d-1})>t</math> or by <math>\max(x_0,\ldots,x_{d-1})>t</math>.

This characterization led to the so-called "definable criterion for definability in Presburger arithmetic", that is: there exists a first-order formula with addition and a {{nowrap|<math>d</math>-ary}} predicate <math>R</math> that holds if and only if <math>R</math> is interpreted by a Presburger-definable relation. Muchnik's theorem also allows one to prove that it is decidable whether an [[automatic sequence]] accepts a Presburger-definable set.

==See also==
*[[Robinson arithmetic]]
*[[Skolem arithmetic]]

==References==
{{Reflist}}

==Bibliography==
{{Refbegin}}

*{{cite journal
 |last= Berman
 |first= L.
 |year= 1980
 |title= The Complexity of Logical Theories
 |journal= [[Theoretical Computer Science (journal)|Theoretical Computer Science]]
 |volume= 11
 |issue= 1
 |pages= 71–77
 |doi= 10.1016/0304-3975(80)90037-7
 |doi-access= free
}}

*{{cite conference
 |last= Büchi
 |first= J. Richard
 |author-link= Julius Richard Büchi
 |year= 1962
 |title= On a Decision Method in Restricted Second Order Arithmetic
 |conference= Proceedings of the International Congress for Logic
 |book-title= Logic, methodology and philosophy of science
 |location= Stanford
 |pages= 1–11
 |publisher= [[Stanford University Press]]
 |editor1-last= Nagel
 |editor1-first= Ernest
 |editor1-link= Ernest Nagel
 |editor2-last= Suppes
 |editor2-first= Patrick
 |editor2-link= Patrick Suppes
 |editor3-last= Tarski
 |editor3-first= Alfred
 |editor3-link= Alfred Tarski
}}

*{{cite journal
 |last= Cobham
 |first= Alan
 |author-link= Alan Cobham (mathematician)
 |year= 1969
 |title= On the base-dependence of sets of numbers recognizable by finite automata
 |journal= Math. Systems Theory
 |volume= 3
 |issue= 2
 |pages= 186–192
 |doi=10.1007/BF01746527
 |s2cid=19792434
}}

*{{Cite journal
 |last= Cooper
 |first= D.C.
 |year= 1972
 |title= Theorem Proving in Arithmetic without Multiplication
 |journal= Machine Intelligence
 |volume= 7
 |editor1-last= Meltzer
 |editor1-first= B.
 |editor2-last= Michie
 |editor2-first= D.
 |publisher= [[Edinburgh University Press]]
 |pages= 91–99
 |url= https://www21.in.tum.de/teaching/logik/SS16/Exercises/Cooper.pdf
}}

*{{cite journal
 |last1= Eisenbrand
 |first1= Friedrich
 |authorlink1=Friedrich Eisenbrand
 |last2= Shmonin
 |first2= Gennady
 |year= 2008
 |title= Parametric Integer Programming in Fixed Dimension
 |journal= [[Mathematics of Operations Research]]
 |volume= 33
 |issue= 4
 |pages= 839–850
 |arxiv= 0801.4336
 |doi= 10.1287/moor.1080.0320 
|s2cid= 15698556
 }}

*{{Cite book
 |last= Enderton
 |first= Herbert
 |year= 2001
 |title= A mathematical introduction to logic
 |publisher= [[Academic Press]]
 |location= Boston, MA
 |edition= 2nd
 |isbn= 978-0-12-238452-3
}}

*{{cite book
 |last1= Ferrante
 |first1= Jeanne
 |author-link1= Jeanne Ferrante
 |last2= Rackoff
 |first2= Charles W.
 |year= 1979
 |title= The Computational Complexity of Logical Theories
 |series= Lecture Notes in Mathematics
 |volume= 718
 |publisher= [[Springer-Verlag]]
 |doi= 10.1007/BFb0062837
 |isbn= 978-3-540-09501-9
 |mr= 0537764
}}

*{{cite conference
 |last1= Fischer
 |first1= Michael J.
 |author-link1= Michael J. Fischer
 |last2= Rabin
 |first2= Michael O.
 |author-link2= Michael O. Rabin
 |year= 1974
 |title= Super-Exponential Complexity of Presburger Arithmetic
 |url= http://www.lcs.mit.edu/publications/pubs/ps/MIT-LCS-TM-043.ps
 |series= SIAM-AMS Proceedings
 |editor-last= Karp
 |editor-first= Richard M.
 |book-title= Complexity of computation
 |publisher= [[American Mathematical Society]]
 |isbn= 978-0-8218-1327-0
 |oclc= 1205569621
 |volume= 7
 |pages= 27–41
 |access-date= 2006-06-11
 |archive-url= https://web.archive.org/web/20060915010325/http://www.lcs.mit.edu/publications/pubs/ps/MIT-LCS-TM-043.ps
 |archive-date= 2006-09-15
 |url-status= dead
}}

*{{cite journal
 |last1= Ginsburg
 |first1= Seymour
 |author-link1= Seymour Ginsburg
 |last2= Spanier
 |first2= Edwin Henry
 |author-link2= Edwin Spanier
 |year= 1966
 |title= Semigroups, Presburger Formulas, and Languages
 |journal= [[Pacific Journal of Mathematics]]
 |volume= 16
 |issue= 2
 |pages= 285–296
 |doi=10.2140/pjm.1966.16.285
 |doi-access=free
|url= https://projecteuclid.org/journals/pacific-journal-of-mathematics/volume-16/issue-2/Semigroups-Presburger-formulas-and-languages/pjm/1102994974.pdf
 }}

*{{cite conference
 | last= Haase
 | first= Christoph
 | year= 2014
 | title= Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy
 | book-title= Proceedings CSL-[[Logic in Computer Science|LICS]]
 | publisher= ACM
 | pages= 47:1–47:10
 | doi= 10.1145/2603088.2603092
 | arxiv= 1401.5266
}}

*{{Cite journal
 |last= Haase
 |first= Christoph
 |year= 2018
 |title= A Survival Guide to Presburger Arithmetic
 |journal= ACM SIGLOG News
 |url= http://www.cs.ox.ac.uk/people/christoph.haase/home/publication/haa-18/haa-18.pdf
 |volume= 5
 |issue= 3
 |pages= 67–82
 |doi= 10.1145/3242953.3242964
 |s2cid= 51847374
}}

*{{cite web
 |last= Hoang
 |first= Nhat Minh
 |title= Presburger Arithmetic
 |url= https://www21.in.tum.de/teaching/sar/SS20/9.pdf
 |at= [[Technical University of Munich|Technische Universität München]]
 |quote= In this paper a procedure for constructing an automaton that decides Presburger arithmetic is explained.
 |access-date= 22 March 2024
}}

*{{cite book
 |last1= King
 |first1= Tim
 |last2= Barrett
 |first2= Clark W.
 |last3= Tinelli
 |first3= Cesare
 |title= 2014 Formal Methods in Computer-Aided Design (FMCAD)
 |year= 2014
 |chapter= Leveraging linear and mixed integer programming for SMT
 |volume= 2014
 |pages= 139–146
 |doi= 10.1109/FMCAD.2014.6987606
 |isbn= 978-0-9835-6784-4
 |s2cid= 5542629
}}

*{{cite journal
 |last1= Michaux
 |first1= Christian
 |last2= Villemaire
 |first2= Roger
 |title= Presburger Arithmetic and Recognizability of Sets of Natural Numbers by Automata: New Proofs of Cobham's and Semenov's Theorems
 |journal= [[Annals of Pure and Applied Logic]]
 |date= 1996
 |volume= 77
 |issue= 3
 |pages= 251–277
 |doi= 10.1016/0168-0072(95)00022-4
 |doi-access= 
}}

*{{Cite book
 |last= Monk
 |first= J. Donald
 |year= 2012
 |title= Mathematical Logic (Graduate Texts in Mathematics (37))
 |publisher= Springer
 |edition= Softcover reprint of the original 1st ed. 1976
 |isbn= 9781468494549
}}

*{{cite journal
 |last= Muchnik
 |first= Andrei A.
 |title= The definable criterion for definability in Presburger arithmetic and its applications
 |journal= Theor. Comput. Sci.
 |date= 2003
 |volume= 290
 |issue= 3
 |pages= 1433–1444
 |doi= 10.1016/S0304-3975(02)00047-6
 |doi-access= free
}}

*{{cite journal
 |last1= Nelson
 |first1= Greg
 |last2= Oppen
 |first2= Derek C.
 |date= April 1978
 |title= A simplifier based on efficient decision algorithms
 |journal= Proc. 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
 |pages= 141–150
 |doi= 10.1145/512760.512775
 |s2cid= 6342372
}}

*{{cite book
 |last1= Nguyen |first1= Danny
 |last2= Pak |first2= Igor |title= 2017 IEEE 58th Annual Symposium on Foundations of Computer Science (FOCS)
 |chapter= Short Presburger Arithmetic is Hard
 |authorlink2=Igor Pak
 |year= 2017
 |pages= 37–48
 |chapter-url= http://www.math.ucla.edu/~pak/papers/hard_presburger3.pdf
 |access-date= 2022-09-04
 |arxiv= 1708.08179
 |doi= 10.1109/FOCS.2017.13 
|isbn= 978-1-5386-3464-6
 |s2cid= 3425421
 }}

*{{cite thesis
 |last= Nguyen Luu
 |first= Dahn
 |year= 2018
 |title= The Computational Complexity of Presburger Arithmetic
 |publisher= UCLA Electronic Theses and Dissertations
 |location= Los Angeles
 |url= https://escholarship.org/uc/item/6j9051vs
 |access-date= 2022-09-08
}}

*{{cite journal
 |last= Nipkow
 |first= T
 |year= 2010
 |title= Linear Quantifier Elimination
 |url= https://www.proof.cit.tum.de/~nipkow/pubs/jar10.pdf
 |journal= [[Journal of Automated Reasoning]]
 |volume= 45
 |issue= 2
 |pages= 189–212
 |doi= 10.1007/s10817-010-9183-0
 |s2cid= 14279141
}}

*{{cite journal
 |last= Oppen
 |first= Derek C.
 |year= 1978
 |title= A 2<sup>2<sup>2<sup>''pn''</sup></sup></sup> Upper Bound on the Complexity of Presburger Arithmetic
 |journal= [[J. Comput. Syst. Sci.]]
 |volume= 16
 |issue= 3
 |pages= 323–332
 |doi= 10.1016/0022-0000(78)90021-1
 |doi-access= free
}}

*{{cite journal
 |last= Presburger
 |first= Mojżesz
 |author-link= Mojżesz Presburger
 |date= 1929
 |title= Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt
 |journal= Comptes Rendus du I congrès de Mathématiciens des Pays Slaves, Warszawa
 |pages= 92–101
}}, see {{harvtxt|Stansifer|1984}} for an English translation

*{{cite conference
 |last= Pugh
 |first= William
 |author-link= William Pugh (computer scientist)
 |title= Proceedings of the 1991 ACM/IEEE conference on Supercomputing - Supercomputing '91
 |chapter= The Omega test: A fast and practical integer programming algorithm for dependence analysis
 |year= 1991
 |pages= 4–13
 |publisher = Association for Computing Machinery
 |publication-place= New York, NY, USA
 |doi= 10.1145/125826.125848
 |isbn= 0897914597
 |s2cid= 3174094
 |citeseerx= 10.1.1.37.1995
 }}

*{{cite conference
 |last1= Reddy
 |first1= C.R.
 |last2= Loveland
 |first2= D.W.
 |title= Proceedings of the tenth annual ACM symposium on Theory of computing - STOC '78
 |chapter= Presburger arithmetic with bounded quantifier alternation
 |year= 1978
 |pages = 320–325
 |doi= 10.1145/800133.804361
 |s2cid= 13966721
}}

*{{cite journal
 |first= A.L.
 |last= Semenov
 |year= 1977
 |title= Presburgerness of predicates regular in two number systems
 |language= ru
 |journal= [[Sibirsk. Mat. Zh.]]
 |volume= 18
 |issue= 2
 |pages= 403–418
|doi= 10.1007/BF00967164
 |bibcode= 1977SibMJ..18..289S
 }}

*{{cite report
 |last= Stansifer
 |first= Ryan
 |date= Sep 1984
 |title= Presburger's Article on Integer Arithmetic: Remarks and Translation
 |type= Technical Report
 |location= Ithaca/NY
 |publisher= Dept. of Computer Science, Cornell University
 |volume= TR84-639
 |url= http://cs.fit.edu/~ryan/papers/presburger.pdf
}}

*{{cite book
 |last= Young
 |first= P.
 |year= 1985
 |contribution= Gödel theorems, exponential difficulty and undecidability of arithmetic theories: an exposition
 |title= Recursion Theory, American Mathematical Society
 |editor= A. Nerode and R. Shore
 |pages= 503–522
}}

*{{cite thesis
 |last= Zoethout
 |first= Jetze
 |date= February 1, 2015
 |title= Interpretations in Presburger Arithmetic (Bachelor Thesis)
 |url= https://studenttheses.uu.nl/bitstream/handle/20.500.12932/20281/Thesis.pdf
 |access-date= 2023-08-25
 }}

{{Refend}}

==External links==
*[http://www.philipp.ruemmer.org/princess.shtml A complete Theorem Prover for Presburger Arithmetic] by Philipp Rümmer

[[Category:1929 introductions]]
[[Category:Formal theories of arithmetic]]
[[Category:Logic in computer science]]
[[Category:Proof theory]]
[[Category:Model theory]]