Presburger arithmetic

Presburger arithmetic is the first-order theory of the natural numbers with addition, named in honor of Mojżesz Presburger, who introduced it in 1929. The signature of Presburger arithmetic contains only the addition operation and equality, omitting the multiplication operation entirely. The theory is computably axiomatizable; the axioms include a schema of induction.

Presburger arithmetic is much weaker than Peano arithmetic, which includes both addition and multiplication operations. Unlike Peano arithmetic, Presburger arithmetic is a 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 computational complexity of this algorithm is at least doubly exponential, however, as shown by Fischer & Rabin (1974).

Overview

The language of Presburger arithmetic contains constants Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle 0} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle 1} and a binary function Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle +} , interpreted as addition.

In this language, the axioms of Presburger arithmetic are the universal closures of the following:

1. Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \neg(0 = x + 1)}
2. Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x + 1 = y + 1 \to x = y}
3. Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x + 0 = x}
4. Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x + (y + 1) = (x + y) + 1}
5. Let Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle P(x)} be a first-order formula in the language of Presburger arithmetic with a free variable Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x} (and possibly other free variables). Then the following formula is an axiom:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (P(0) \land \forall x(P(x) \to P(x+1))) \to \forall y\, P(y).}

(5) is an axiom schema of 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.

Presburger arithmetic can be viewed as a 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 intended interpretation: the structure of non-negative integers with constants Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle 0} , Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle 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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): \forall x\, \exists y\; ((y + y = x) \lor (y + y + 1 = x)). This states that every number is either even or odd.

Properties

Presburger (1929) proved Presburger arithmetic to be:

• consistent: There is no statement in Presburger arithmetic that can be deduced from the axioms such that its negation can also be deduced.
• 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.
• 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 the two definitions are equivalent.

The decidability of Presburger arithmetic can be shown using quantifier elimination, supplemented by reasoning about arithmetical congruence. 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.

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 Fischer & Rabin (1974) proved that, in the worst case, the proof of the statement in first-order logic has length at least Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle 2^{2^{cn}}} , 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 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.

Recent work has also considered functional synthesis problems over Presburger arithmetic, including the identification of restricted fragments with more efficient solution procedures.

On the other hand, a triply exponential upper bound on a decision procedure for Presburger arithmetic was proved by Oppen.

A more tight complexity bound was shown using alternating complexity classes by Berman (1980). The set of true statements in Presburger arithmetic (PA) is shown complete for TimeAlternations(2^2nO(1), n). Thus, its complexity is between double exponential nondeterministic time (2-NEXP) and double exponential space (2-EXPSPACE). Completeness is under Karp reductions. (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 Σ_i PA statements, and PA(i, j) the set of true Σ_i PA statements with each quantifier block limited to j variables. '<' is considered to be quantifier-free; here, bounded quantifiers are counted as quantifiers.
PA(1, j) is in P, while PA(1) is NP-complete.
For i > 0 and j > 2, PA(i + 1, j) is Σ_i^P-complete. The hardness result only needs j>2 (as opposed to j=1) in the last quantifier block.
For i>0, PA(i+1) is Σ_i^EXP-complete.

Short Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Sigma_n} Presburger Arithmetic (Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle n>2} ) is Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Sigma_{n-2}^P} complete (and thus NP complete for Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle n=3} ). Here, 'short' requires bounded (i.e. Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle O(1)} ) sentence size except that integer constants are unbounded (but their number of bits in binary counts against input size). Also, Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Sigma_2} two variable PA (without the restriction of being 'short') is NP-complete. Short Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Pi_2} (and thus Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Sigma_2} ) PA is in P, and this extends to fixed-dimensional parametric integer linear programming.

Applications

Because Presburger arithmetic is decidable, automatic theorem provers for Presburger arithmetic exist. For example, the Rocq and Lean proof assistant systems feature the tactic omega for Presburger arithmetic and the Isabelle proof assistant contains a verified quantifier elimination procedure by 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: 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.

Presburger arithmetic can express multiplication by constants, as an abbreviation for iterated addition: Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle cx = \underbrace{x + x + \cdots + x}_{c\text{ times}} .} Most array subscript calculations then fall within the region of decidable problems. This approach is the basis of at least five proof-of-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 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.

A unary integer relation Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle R} , 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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t\in \N} and a positive period Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle p\in\N^{>0}} such that, for all integer Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle n} such that Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle |n|\ge t} , Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle n\in R} if and only if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle n+p\in R} .

By the Cobham–Semenov theorem, a relation is Presburger-definable if and only if it is definable in Büchi arithmetic of base Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle k} for all Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle k\ge2} . A relation definable in Büchi arithmetic of base Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle k} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle k'} for Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle k} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle k'} being multiplicatively independent integers is Presburger definable.

An integer relation Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle R} is Presburger-definable if and only if all sets of integers that are definable in first-order logic with addition and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle R} (that is, Presburger arithmetic plus a predicate for Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle R} ) are Presburger-definable. Equivalently, for each relation Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle R} that is not Presburger-definable, there exists a first-order formula with addition and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle R} that defines a set of integers that is not definable using only addition.

An integer function is Presburger-definable if and only if it is piecewise linear on a semilinear partition of its domain, with each linear piece having a periodic component.

Muchnik's characterization

Presburger-definable relations admit another characterization: by Muchnik's theorem. 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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle R\subseteq\N^d} be a set, the section Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x_i = j} of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle R} , for Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle i < d} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle j \in \N} is defined as

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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 \}.}

Given two sets Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle R,S\subseteq\N^d} and a Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle d} -tuple of integers Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (p_0,\ldots,p_{d-1})\in\N^d} , the set Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle R} is called Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (p_0,\dots,p_{d-1})} -periodic in Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle S} if, for all Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (x_0, \dots, x_{d-1}) \in S} such that Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (x_0+p_0,\dots,x_{d-1}+p_{d-1})\in S,} then Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (x_0,\ldots,x_{d-1})\in R} if and only if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (x_0+p_0,\dots,x_{d-1}+p_{d-1})\in R} . For Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle s\in\N} , the set Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle R} is said to be Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle s} -periodic in Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle S} if it is Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (p_0,\ldots,p_{d-1})} -periodic for some Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (p_0,\dots,p_{d-1})\in\Z^d} such that

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \sum_{i=0}^{d-1}|p_i| < s.}

Finally, for Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle k,x_0,\dots,x_{d-1}\in\N} let

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle 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 \}}

denote the cube of size Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle k} whose lesser corner is Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (x_0,\dots,x_{d-1})} .

Intuitively, the integer Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle s} represents the length of a shift, the integer Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle k} is the size of the cubes and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t} is the threshold before the periodicity. This result remains true when the condition

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \sum_{i=0}^{d-1}x_i>t}

is replaced either by Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \min(x_0,\ldots,x_{d-1})>t} or by Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \max(x_0,\ldots,x_{d-1})>t} .

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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle d} -ary predicate Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle R} that holds if and only if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle R} 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
• Elementary recursive function

Bibliography

• Akshay, S.; Balasubramanian, A. R.; Chakraborty, S.; Zetzsche, G. (2025). "Presburger Functional Synthesis: Complexity and Tractable Normal Forms" (PDF). Proceedings of the 22nd International Conference on Principles of Knowledge Representation and Reasoning (KR 2025).

• Berman, L. (1980). "The Complexity of Logical Theories". Theoretical Computer Science. 11 (1): 71–77. doi:10.1016/0304-3975(80)90037-7.

• Büchi, J. Richard (1962). "On a Decision Method in Restricted Second Order Arithmetic". In Nagel, Ernest; Suppes, Patrick; Tarski, Alfred (eds.). Logic, methodology and philosophy of science. Proceedings of the International Congress for Logic. Stanford: Stanford University Press. pp. 1–11.

• Cobham, Alan (1969). "On the base-dependence of sets of numbers recognizable by finite automata". Math. Systems Theory. 3 (2): 186–192. doi:10.1007/BF01746527. S2CID 19792434.

• Cooper, D.C. (1972). Meltzer, Bernard; Michie, Donald (eds.). "Theorem Proving in Arithmetic without Multiplication" (PDF). Machine Intelligence. Edinburgh: Edinburgh University Press. 7: 91–99. Retrieved 17 March 2026.

• Eisenbrand, Friedrich; Shmonin, Gennady (2008). "Parametric Integer Programming in Fixed Dimension". Mathematics of Operations Research. 33 (4): 839–850. arXiv:0801.4336. doi:10.1287/moor.1080.0320. S2CID 15698556.

• Enderton, Herbert (2001). A mathematical introduction to logic (2nd ed.). Boston, MA: Academic Press. ISBN 978-0-12-238452-3.

• Ferrante, Jeanne; Rackoff, Charles W. (1979). The Computational Complexity of Logical Theories. Lecture Notes in Mathematics. 718. Springer-Verlag. doi:10.1007/BFb0062837. ISBN 978-3-540-09501-9. MR 0537764.

• Finkel, Alain; Leroux, Jérôme (March 2008). Presburger Functions are Piecewise Linear (PDF) (Research report). Laboratoire Spécification et Vérification, ENS Cachan. LSV-08-08.

• Fischer, Michael J.; Rabin, Michael O. (1974). "Super-Exponential Complexity of Presburger Arithmetic". In Karp, Richard M. (ed.). Complexity of computation. SIAM-AMS Proceedings. 7. American Mathematical Society. pp. 27–41. ISBN 978-0-8218-1327-0. OCLC 1205569621. Archived from the original on 15 September 2006. Retrieved 11 June 2006.

• Ginsburg, Seymour; Spanier, Edwin Henry (1966). "Semigroups, Presburger Formulas, and Languages" (PDF). Pacific Journal of Mathematics. 16 (2): 285–296. doi:10.2140/pjm.1966.16.285.

• Haase, Christoph (2014). "Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy". Proceedings CSL-LICS. ACM. pp. 47:1–47:10. arXiv:1401.5266. doi:10.1145/2603088.2603092.

• Haase, Christoph (2018). "A Survival Guide to Presburger Arithmetic" (PDF). ACM SIGLOG News. 5 (3): 67–82. doi:10.1145/3242953.3242964. S2CID 51847374.

• Hoang, Nhat Minh. "Presburger Arithmetic" (PDF). Technische Universität München. Retrieved 22 March 2024. In this paper a procedure for constructing an automaton that decides Presburger arithmetic is explained.

• King, Tim; Barrett, Clark W.; Tinelli, Cesare (2014). "Leveraging linear and mixed integer programming for SMT". 2014 Formal Methods in Computer-Aided Design (FMCAD). 2014. pp. 139–146. doi:10.1109/FMCAD.2014.6987606. ISBN 978-0-9835-6784-4. S2CID 5542629.

• Michaux, Christian; Villemaire, Roger (1996). "Presburger Arithmetic and Recognizability of Sets of Natural Numbers by Automata: New Proofs of Cobham's and Semenov's Theorems". Annals of Pure and Applied Logic. 77 (3): 251–277. doi:10.1016/0168-0072(95)00022-4.

• Monk, J. Donald (2012). Mathematical Logic (Graduate Texts in Mathematics (37)) (Softcover reprint of the original 1st ed. 1976 ed.). Springer. ISBN 9781468494549.

• Muchnik, Andrei A. (2003). "The definable criterion for definability in Presburger arithmetic and its applications". Theor. Comput. Sci. 290 (3): 1433–1444. doi:10.1016/S0304-3975(02)00047-6.

• Nelson, Greg; Oppen, Derek C. (April 1978). "A simplifier based on efficient decision algorithms". Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages - POPL '78. pp. 141–150. doi:10.1145/512760.512775. S2CID 6342372.

• Nguyen, Danny; Pak, Igor (2017). "Short Presburger Arithmetic is Hard" (PDF). 2017 IEEE 58th Annual Symposium on Foundations of Computer Science (FOCS). pp. 37–48. arXiv:1708.08179. doi:10.1109/FOCS.2017.13. ISBN 978-1-5386-3464-6. S2CID 3425421. Retrieved 4 September 2022.

• Template:Cite thesis

• Nipkow, T (2010). "Linear Quantifier Elimination" (PDF). Journal of Automated Reasoning. 45 (2): 189–212. doi:10.1007/s10817-010-9183-0. S2CID 14279141.

• Oppen, Derek C. (1973). "Elementary Bounds for Presburger Arithmetic". Proceedings of the Fifth Annual ACM Symposium on Theory of Computing (STOC ’73). pp. 34–37. doi:10.1145/800125.804033.

• Oppen, Derek C. (1978). "A 2^22pn Upper Bound on the Complexity of Presburger Arithmetic". J. Comput. Syst. Sci. 16 (3): 323–332. doi:10.1016/0022-0000(78)90021-1.

• Podnieks, Kārlis (25 January 2015). What is Mathematics: Gödel's Theorem and Around. University of Latvia. doi:10.13140/RG.2.2.24155.77609. Hyper-textbook for students

• Presburger, Mojżesz (1929). "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt". Comptes Rendus du I congrès de Mathématiciens des Pays Slaves, Warszawa: 92–101., see Stansifer (1984) for an English translation

• Pugh, William (1991). "The Omega test: A fast and practical integer programming algorithm for dependence analysis". Proceedings of the 1991 ACM/IEEE conference on Supercomputing - Supercomputing '91. New York, NY, USA: Association for Computing Machinery. pp. 4–13. CiteSeerX 10.1.1.37.1995. doi:10.1145/125826.125848. ISBN 0897914597. S2CID 3174094.

• Reddy, C.R.; Loveland, D.W. (1978). "Presburger arithmetic with bounded quantifier alternation". Proceedings of the tenth annual ACM symposium on Theory of computing - STOC '78. pp. 320–325. doi:10.1145/800133.804361. S2CID 13966721.

• Semenov, A.L. (1977). "Presburgerness of predicates regular in two number systems". Sibirsk. Mat. Zh. (in Russian). 18 (2): 403–418. Bibcode:1977SibMJ..18..289S. doi:10.1007/BF00967164.

• Stansifer, Ryan (September 1984). Presburger's Article on Integer Arithmetic: Remarks and Translation (PDF) (Technical Report). TR84-639. Ithaca/NY: Dept. of Computer Science, Cornell University.

• Young, P. (1985). "Gödel theorems, exponential difficulty and undecidability of arithmetic theories: an exposition". In A. Nerode and R. Shore (ed.). Recursion Theory, American Mathematical Society. pp. 503–522.

• Template:Cite thesis

External links

• A complete Theorem Prover for Presburger Arithmetic by Philipp Rümmer