Presburger arithmetic

The Presburger arithmetic is a formulated in the first order predicate logic mathematical theory of natural numbers with addition. It is named after Mojżesz Presburger, who introduced it in 1929. The signature of the arithmetic Presburger includes only addition, but not the multiplication. For axiom system includes an axiom schema of complete induction.

The Presburger arithmetic is significantly weaker than Peano arithmetic, be formalized in both addition and multiplication. In contrast to Peano arithmetic that Presburger arithmetic is a decidable theory, that is, it can be formulated for each in the language of Presburger arithmetic statement effectively decide whether it is provable from the axioms of the theory or not. However, the asymptotic running time of a corresponding algorithm is doubly exponential, according to a study by Fischer and Rabin.

Definition

Language Presburger arithmetic contains constants 0 and 1, and a binary operation that can be interpreted as addition. In this language, the axioms of Presburger arithmetic are as follows:

The latter is an axiom scheme of induction and represents an infinite number of individual axioms. This the scheme ( 6) corresponding axioms can not be replaced by a finite number of axioms, so that Presburger arithmetic is not finite total axiomatizable.

Description

The Presburger arithmetics, concepts such as divisibility or prime numbers not formalize, let alone the multiplication, because then would have to Presburger arithmetic as the Peano arithmetic is incomplete and undecidable. Individual instances of divisibility can be formalized but well, such as " Just Be" by; hereby expressible true statements as

Are then provable sentences.

Properties

Mojżesz Presburger had the following properties of its arithmetic by:

• Consistency: There is no formulated in their language statement, for which it can be deduced both from the axioms.
• Completeness: For each formulated in the language of Presburger arithmetic statement is either the denial or derivable from the axioms.
• Decidability: There is an algorithm that can decide at any given statement Presburger arithmetic, whether it is true or false.

The decidability of Presburger arithmetic can be proved by quantifier elimination and the consideration of arithmetic congruences.

The Peano arithmetic, so Presburger arithmetic plus multiplication, however, is not decidable. According to Gödel's incompleteness theorem, it is also incomplete, and their consistency is not provable (internal).

The decision problem for Presburger arithmetic is an interesting example of the complexity theory. Let the length of a statement of Presburger arithmetic. Then the decision algorithm for Presburger Arithmetic has at least double-exponential running time according to a study by Fischer and Rabin, ie in the worst case, the running time at least for a certain positive constant. On the other hand, there is a triple- exponential upper bound for the running time. It is a decision problem that has been proven can not be solved in exponential (let alone polynomial ) time. Fischer and Rabin also showed that for any reasonable ( in one of them präzisierten sense) axiomatization sets of any length exist whose shortest proof of double - exponential length. Intuitively, this means that there are practical limits to the computer proof. From the work of Fischer and Rabin is also clear that with Presburger arithmetic formulas can be defined that simulate any algorithm correct as long as the inputs certain - do not cross borders - relatively high. These limits can be increased by the transition to other formulas, respectively.

Applications

There are actually computer proof systems that make use of algorithms for deciding formulas in Presburger arithmetic. Example, contains Coq proof tactics in this direction. Although the double-exponential complexity limits the practical applicability of complicated formulas, but this behavior occurs only with nested quantifiers: Oppen and Nelson describe a system based on the simplex method automatic proof system for an extended Presburger arithmetic without nested quantifiers. The worst-case running time of the simplex method is ( simple) exponential. Indeed exponential term is observed even for cases specially designed, while it operates much more efficiently in daily life circumstances. Thus, this approach is quite suitable for practical use.

The Presburger arithmetic can be extended to multiplication by constants, since this is repeated addition. In the programming technique, this concerns for example the calculation of array indices. This approach is based on at least five systems for the proof of correctness of computer programs, starting with the Stanford Pascal Verifier from the late 1970s through to Microsoft Spec # of 2005.