PresburgerArithmetic is the FirstOrderTheory of the natural numbers containing addition but no multiplication. It is therefore not as powerful as PeanoArithmetic. However, it is interesting because unlike the case of PeanoArithmetic, there exists an algorithm that can decide if any given statement in PresburgerArithmetic is true (Presburger 1929). No such algorithm exists for general arithmetic as a consequence of Robinson and Tarski's negative answer to the decision problem. Presburger (1929) also proved that his arithmetic is consistent (does not contain contradictions) and complete (every statement can either be proven or disproven), which is false for Peano arithmetic as a consequence of Gödel's incompleteness theorem.
Fischer and Rabin (1974) proved that every algorithm which decides the truth of Presburger statements has a running time of at least attachment:bound.jpg for some constant c, where n is the length of the Presburger statement. Therefore, the problem is one of the few currently known that provably requires more than polynomial run time.
See
attachment:PresburgerAxioms.pdf < attachment:PresburgerAxioms.tex
[http://mathworld.wolfram.com/PresburgerArithmetic.html Mathworld: Presburger Arithmetic]
[http://www.e-paranoids.com/p/pr/presburger_arithmetic.html Axioms of Presburger Arithmetic]
[http://mathworld.wolfram.com/PeanoArithmetic.html Peano Arithmetic]