Presburger-Arithmetik

Dieser Importartikel ist fälschlicherweise im Artikelnamensraum. Bitte verschiebe die Seite oder entferne diesen Baustein.

Dieser Artikel (Presburger-Arithmetik) ist im Entstehen begriffen und noch nicht Bestandteil der freien Enzyklopädie Wikipedia.

Wenn du dies liest:

• Der Text kann teilweise in einer Fremdsprache verfasst, unvollständig sein oder noch ungeprüfte Aussagen enthalten.
• Wenn du Fragen zum Thema hast, nimm am besten Kontakt mit den Autoren auf.

Wenn du diesen Artikel überarbeitest:

• Bitte denke daran, die Angaben im Artikel durch geeignete Quellen zu belegen und zu prüfen, ob er auch anderweitig den Richtlinien der Wikipedia entspricht (siehe Wikipedia:Artikel).
• Nach erfolgter Übersetzung kannst du diese Vorlage entfernen und den Artikel in den Artikelnamensraum verschieben. Die entstehende Weiterleitung kannst du schnelllöschen lassen.
• Importe inaktiver Accounts, die länger als drei Monate völlig unbearbeitet sind, werden gelöscht.

Vorlage:Importartikel/Wartung-2012-02

Die Presburger-Arithmetik ist eine in der Prädikatenlogik erster Stufe formulierte mathematische Theorieder natürlichen Zahlen mit Addition. Sie ist benannt nach Mojżesz Presburger, der sie im Jahre 1929 einführte. Die Signatur der Presburger-Arithmetik beinhält nur Addition und Gleichheit, nicht jedoch die Multiplikation. Zum Axiomensystem gehört auch ein Axiomenschema der vollständigen Induktion.

Die Presburger-Arithmetik ist erheblich schwächer als die Peano-Arithmetik, in der sowohl Addition als auch Multiplikaiton formalisiert werden. Im Gegensatz zur Peano-Arithmetik ist die Presburger-Arithmetik eine entscheidbare Theorie, d. h. es lässt sich für jede in der Sprache der Presburger-Arithmetik formulierte Aussage effektiv entscheiden, ob sie aus den Axiomen der Theorie beweisbar ist oder nicht. Allerdings ist die asymptotische Laufzeit eines entsprechenden Algorithmus laut einer Arbeit von Fischer und Rabin doppelt exponentiell.

Beschreibung

Die Sprache der Presburger-Arithmetik enthält Konstanten 0 und 1 sowie eine binäre Operation +, die als Addition zu interpretieren ist. In dieser Sprache lauten die Axiome der Presburger-Arithmetik wie folgt:

1. $\forall x\colon \neg (x+1=0)$
2. $\forall x,y\colon (x+1=y+1\rightarrow x=y$
3. $\forall x\colon x+0=x$
4. $\forall x,y\colon (x+y)+1=x+(y+1)$
5. Sei $P(x,y_{1},\ldots ,y_{k})$ eine Formel in der Sprache der Presburger-Arithmetik mit freien Variablen $x,y_{1},\ldots ,y_{k}$. Dann ist folgende Aussage ein Axiom:

$\forall y_{1},\ldots ,y_{k}\colon ((P(0,y_{1},\ldots ,y_{k})\land \forall x\colon (P(x,y_{1},\ldots ,y_{k})\rightarrow P(x+1,y_{1},\ldots ,y_{k})))\rightarrow \forall x\colon P(x,y_{1},\ldots ,y_{k}))$

Letzteres ist ein Axiomenschema der vollständigen Induktion und steht für unendlich viele Einzelaxiome. Diese dem Schema (5) entsprechenden Axiome lassen sich nicht durch endlich viele Axiome ersetzen, so dass die Presburger-Arithmetik insgesamt nicht endlich axiomatisierbar ist.

Die Presburger-Arithmetik kann Konzepte wie Teilbarkeit oder Primzahlen nicht formalisieren, geschweige denn die Multiplikation, denn dann müsste die Presburger-Arithmetik wie die Peano-Arithmetik unvollständig und unentscheidbar sein. Individuelle Instanzen der Teilbarkeit können aber durchaus formalisiert werden, etwa „$x$ ist gerade“ durch $G(x):\Leftrightarrow \exists z\colon z+z=x$; hiermit ausdrückbare wahre Aussagen wie

$\forall x,y\colon (G(x)\land G(y)\rightarrow G(x+y))$

(„Die Summe zweier gerader Zahlen ist gerade“)

sind dann beweisbare Sätze.

Eigenschaften

Mojżesz Presburger wies folgende Eigenschaften der seiner Arithmetik nach:

• Konsistenz: Es gibt keine in ihrer Sprache formulierte Aussage $P$, für die sowohl $P$ als auch $\neg P$ aus den Axiomen hergeleitet werden kann.
• Vollständigkeit: Für jede in der Sprache der Presburger-Arithmetik formulierte Aussage $P$ ist entweder $P$ oder die Verneinung $\neg P$ aus den Axiomen herleitbar.
• Entscheidbarkeit: Es gibt einen Algorithmus, der zu jeder gegebenen Aussage der Presburger-Arithmetik entscheiden kann, ob sie wahr oder falsch ist.

Die Entscheidbarkeit der Presburger-Arithmetik lässt sich durch Quantorenelimination und die Betrachtung arithmetischer Kongruenzen nachweisen.

Die Peano-Arithmetik, also Presburger-Arithmetik zuzüglich Multiplikation, ist dagegen nicht entscheidbar. Gemäß Gödels Unvollständigkeitssatz ist sie auch unvollständig und ihrer Konsistenz nicht (intern) beweisbar.

Das Entscheidungsproblem für die Presburger-Arithmetik ist ein interessantes Beispiel der Komplexitätstheorie. Sei $n$ die Länge einer Aussage der Presburger-Arithmetik. Dann hat der Entscheidungsalgorithmus für die Presburger-Arithmetik laut einer Arbeit von Fischer und Rabin mindestens doppelt-exponentielle Laufzeit, d. h. im worst case beträgt die Laufzeit mindestens $2^{2^{cn}}$ für eine gewisse positive Konstante $c$. Andererseits gibt es eine dreifach-exponentielle obere Abschätzung für die Laufzeit. Es handelt sich also um ein Entscheidungsproblem, das nachweislich nicht in exponentieller (geschweige denn polynomieller) Zeit gelöst werden kann. Fischer und Rabin zeigten auch, dass für jede (in einem von ihnen präzisierten Sinne) vernünftige Axiomatisierung Sätze beliebiger Länge existieren, deren kürzester Beweis von doppelt-exponentieller Länge ist. Intuitiv bedeutet dies, dass es praktische Grenzen für Computerbeweise gibt. Aus der Arbeit von Fischer und Rabin ergibt sich ferner, dass mit der Presburger-Arithmetik Formeln definiert werden können, die einen beliebigen Algorithmus korrekt nachbilden, solange die Eingaben gewisse – verhältnismäßig hohe – Grenzen nicht überschreiten. Diese Grenzen können durch den Übergang zu anderen Formeln jeweils noch erhöht werden.

Anwendungen

Da die Presburger-Arithmetik entscheidbar ist, gibt es Computerbeweissysteme für sie. Beispielsweise enthält Coq Beweistaktiken in dieser Richtung. Die doppelt-exponentielle Komplexität begrenzt zwar die praktische Einsetzbarkeit für komplizierte Formeln, jedoch tritt dieses Verhalten nur bei verschachtelten Quantoren auf: Oppen und Nelson beschreiben ein auf dem Simplexverfahren beruhendes automatisches Beweissystem für eine erweiterte Presburger-Arithmetik ohne verschachtelte Quantoren. Die Worst-case-Laufzeit des Simplexverfahrens ist (einfach) exponentiell. Tatsächlich wird exponentielle Laufzeit sogar nur für speziell konstruierte Fälle beobachtet, während es in Alltagsfällen erheblich effizienter arbeitet. Hierdurch ist dieser Ansatz durchaus für den praktischen Einsatz geeignet.

Die Presburger-Arithmetik lässt sich um die Multiplikation mit Konstanten erweitern, da es sich hierbei um wiederholte Addition handelt. In der Programmiertechnik betrifft dies beispielsweise die Berechnung von Feldindizes. Dieser Ansatz ist Grundlage von mindestens fünf Systemen für den Korrektheitsbeweis von Computerprogrammen, angefangen beim Stanford Pascal Verifier aus den späten 1970er Jahren bis hin zu Microsofts Spec# von 2005.

Siehe auch

• Robinson-Arithmetik

Literatur

• David C. Cooper: Theorem Proving in Arithmetic without Multiplication. In: Bernhard Meltzer und Donald Michie (Hrsg.): Machine Intelligence. Band 7. Edinburgh University Press, Edinburgh 1972, ISBN 978-0-470-60110-5, S. 91–100. 
• Jeanne Ferrante und Charles W. Rackoff: The Computational Complexity of Logical Theories (= Lecture Notes in Mathematics. Nr. 718). Springer-Verlag, 1979, ISBN 978-3-540-09501-9. 
• William Pugh: The Omega test. a fast and practical integer programming algorithm for dependence analysis. In: Proceedings of the 1991 ACM/IEEE conference on Supercomputing. 1991, ISBN 0-89791-459-7, doi:10.1145/125826.125848. 
• Cattamanchi Ramalinga Reddy und Donald W. Loveland: Presburger Arithmetic with Bounded Quantifier Alternation. In: ACM Symposium on Theory of Computing. 1978, S. 320–325, doi:10.1145/800133.804361. 
• Paul Young: Gödel theorems, exponential difficulty and undecidability of arithmetic theories. an exposition. In: Anil Nerode und Richard A. Shore (Hrsg.): Recursion Theory (= Proceedings of symposia in pure mathematics). Band 42. American Mathematical Society, 1985, ISBN 978-0-8218-1447-5, S. 503–522. 

Weblinks

• Stefan Baur, Studienarbeit mit einem Java-Applet zum Beweisen, Widerlegen oder Vereinfachen beliebiger Formeln der Presburger Arithmetik.
• Philipp Rümmer, Princess, ein Computerbeweissystem für Presburger-Arithmetik (englisch).