Presburger arithmetic

From Free net encyclopedia

Presburger arithmetic is the first-order theory of the natural numbers with addition. It is not as powerful as Peano arithmetic because multiplication is omitted. In fact, Mojzesz Presburger proved in 1929 that Presburger arithmetic is decidable. In other words, there is an algorithm which decides for any given statement in Presburger arithmetic whether it is provable or not. No such algorithm exists for general arithmetic as a consequence of the negative answer to the Entscheidungsproblem. Furthermore, Presburger proved that his arithmetic is consistent (does not contain contradictions) and complete (every statement can either be proven or disproven). Again, such a proof cannot be given for general arithmetic; in fact, it follows from Gödel's incompleteness theorem that (any recursive axiomatization of) general arithmetic cannot be both consistent and complete.

The decidability of Presburger arithmetic can be shown using quantifier elimination.

Presburger arithmetic is an interesting example in computational complexity theory and computation because Fischer and Rabin proved in 1974 that every algorithm which decides the truth of Presburger statements has a worst case runtime of at least <math>2^{2^{cn}}</math> for some constant c. Here, n is the length of the Presburger statement. Hence, the problem is one of the few that provably need more than polynomial run time (indeed, even more than exponential time!).

In the formal description of the theory, we use the object constants 0 and 1, the function constant +, and the predicate constant =. The axioms are:

  1. ∀ x : ¬ (0 = x + 1)
  2. ∀ x ∀ y : ¬ (x = y) ⇒ ¬ (x + 1 = y + 1)
  3. ∀ x : x + 0 = x
  4. ∀ x ∀ y : (x + y) + 1 = x + (y + 1)
  5. This is an axiom scheme consisting of infinitely many axioms. If P(x) is any formula involving the constants 0, 1, +, = and a single free variable x, then the following formula is an axiom:
( P(0) ∧ ∀ x : P(x) ⇒ P(x + 1) ) ⇒ ∀ x : P(x)

Concepts such as divisibility or prime number cannot be formalized in Presburger arithmetic. Here is a typical theorem that can be proven from the above axioms:

∀ x ∀ y : ( (∃ z : x + z = y + 1) ⇒ (∀ z : ¬ (((1 + y) + 1) + z = x) ) )

It says that if x ≤ y + 1, then y + 2 > x.

[edit]

Applications

Because Presburger arithmetic is decidable, a decision procedure can be constructed for it. Thus, an automatic theorem prover which will reliably produce a correct result for such problems is possible.

Such theorem provers exist. (Oppen and Nelson 1980) describes an automatic theorem prover which uses the simplex algorithm on an extended Presburger arithmetic.

The simplex algorithm has exponential worst-case run time. But the average run time is far better. Exponential run time is only observed for specially constructed cases. This makes a simplex-based approach practical in a working system.

Presburger arithmetic can be extended to include multiplication by constants, since addition is repeated multiplication. Most 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 though to Microsoft's Spec# system of 2005.

[edit]

References

  • M. Presburger: "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt". In Comptes Rendus du I congrès de Mathématiciens des Pays Slaves, Warszawa, 1929, pp.92-101
  • M.J. Fischer, M.O.Rabin: "Super-Exponential Complexity of Presburger Arithmetic". Proceedings of the SIAM-AMS Symposium in Applied Mathematics, 1974, vol. 7, pp.27-41
  • C. R. Reddy and D. W. Loveland: "Presburger Arithmetic with Bounded Quantifier Alternation". ACM Symposium on Theory of Computing,, 1978, pp.320-325
  • Jeanne Ferrante and Charles W. Rackoff: "The Computational Complexity of Logical Theories". Lecture Notes in Mathematics 718. Springer. 1979.
  • D. C. Cooper: "Theorem Proving in Arithmetic without Multiplication". In B. Meltzer and D. Michie (eds.): Machine Intelligence,, Edinburgh University Press, 1972. pp.91-100
  • William Pugh: "The Omega test: a fast and practical integer programming algorithm for dependence analysis", 1991. http://doi.acm.org/10.1145/125826.125848 .
  • Template:Cite journalfr:Arithmétique de Presburger
Retrieved from "http://www.netipedia.com/index.php/Presburger_arithmetic"