Arithmetik von Presburger ist die Theorie der ersten Ordnung der natürlichen Zahlen mit der Hinzufügung, die zu Ehren von Mojżesz Presburger genannt ist, wer es 1929 eingeführt hat. Die Unterschrift der Arithmetik von Presburger enthält nur die Hinzufügungsoperation und Gleichheit, die Multiplikationsoperation völlig weglassend. Die Axiome schließen ein Diagramm der Induktion ein.

Arithmetik von Presburger ist viel schwächer als Arithmetik von Peano, die sowohl Hinzufügungs-als auch Multiplikationsoperationen einschließt. Verschieden von der Peano Arithmetik ist Arithmetik von Presburger eine entscheidbare Theorie. Das bedeutet, dass es möglich ist, für jeden Satz auf der Sprache der Arithmetik von Presburger effektiv zu bestimmen, ob dieser Satz von den Axiomen der Arithmetik von Presburger nachweisbar ist. Die asymptotische Laufzeit rechenbetonte Kompliziertheit dieses Entscheidungsproblems, ist jedoch, wie gezeigt, durch Fischer und Rabin (1974) doppelt Exponential-.

Übersicht

Die Sprache der Arithmetik von Presburger enthält Konstanten 0 und 1 und eine binäre Funktion +, interpretiert als Hinzufügung. Auf dieser Sprache sind die Axiome der Arithmetik von Presburger die universalen Verschlüsse des folgenden:

1. ¬ (0 = x + 1)
2. x + 1 = y + 1  x = y
3. x + 0 = x
4. (x + y) + 1 = x + (y + 1)
5. Lassen Sie P (x) eine Formel der ersten Ordnung auf der Sprache der Arithmetik von Presburger mit einer freien Variable x (und vielleicht anderen freien Variablen) sein. Dann ist die folgende Formel ein Axiom:

:: (P (0) ∧ ∀x (P (x) → P (x + 1))) → ∀y P (y).

(5) ist ein Axiom-Diagramm der Induktion, ungeheuer viele Axiome vertretend. Da die Axiome im Diagramm in (5) durch keine begrenzte Zahl von Axiomen ersetzt werden können, ist Arithmetik von Presburger nicht begrenzt axiomatizable.

Arithmetik von Presburger kann Konzepte wie Teilbarkeit oder Primzahl nicht formalisieren. Allgemein kann jedes Zahl-Konzept, das zu Multiplikation führt, nicht in der Arithmetik von Presburger definiert werden, da das zu Unvollständigkeit und Unentscheidbarkeit führt. Jedoch kann es individuelle Beispiele der Teilbarkeit formulieren; zum Beispiel erweist es sich "für den ganzen x, dort besteht y: (y + y = x)  (y + y + 1 = x)". Das stellt fest, dass jede Zahl entweder sogar oder seltsam ist.

Eigenschaften

Mojżesz Presburger hat Arithmetik von Presburger bewiesen, um zu sein:

• konsequent: Es gibt keine Behauptung in der Arithmetik von Presburger, die aus den solchen Axiomen abgeleitet werden kann, dass seine Ablehnung auch abgeleitet werden kann.
• abgeschlossen: Für jede Behauptung in der Arithmetik von Presburger ist entweder es möglich, es von den Axiomen abzuleiten, oder es ist möglich, seine Ablehnung abzuleiten.
• entscheidbar: Dort besteht ein Algorithmus, der entscheidet, ob gegebene Behauptung in der Arithmetik von Presburger wahr oder falsch ist.

Die Entscheidbarkeit der Arithmetik von Presburger kann mit quantifier Beseitigung gezeigt werden, die durch das Denken über die arithmetische Kongruenz ergänzt ist (Enderton 2001, p. 188).

Arithmetik von Peano, die mit der Multiplikation vermehrte Arithmetik von Presburger ist, ist demzufolge der negativen Antwort auf Entscheidungsproblem nicht entscheidbar. Durch den Unvollständigkeitslehrsatz von Gödel ist Arithmetik von Peano unvollständig, und seine Konsistenz ist nicht innerlich nachweisbar.

Das Entscheidungsproblem für die Arithmetik von Presburger ist ein interessantes Beispiel in der rechenbetonten Kompliziertheitstheorie und Berechnung. Lassen Sie n die Länge einer Behauptung in der Arithmetik von Presburger sein. Dann haben Fischer und Rabin (1974) bewiesen, dass jeder Entscheidungsalgorithmus für die Arithmetik von Presburger eine Grenzfall-Durchlaufzeit mindestens, für einen unveränderlichen c> 0 hat. Folglich ist das Entscheidungsproblem für die Arithmetik von Presburger ein Beispiel eines Entscheidungsproblems, das, wie man bewiesen hat, mehr verlangt hat als Exponentialdurchlaufzeit. Fischer und Rabin haben auch bewiesen, dass für jeden angemessenen axiomatization (definiert genau in ihrer Zeitung), dort Lehrsätze der Länge n bestehen Sie, die doppelt Exponentiallänge-Beweise haben. Intuitiv bedeutet das, dass es rechenbetonte Grenzen darauf gibt, was durch Computerprogramme bewiesen werden kann. Fischer und die Arbeit von Rabin deuten auch an, dass Arithmetik von Presburger verwendet werden kann, um Formeln zu definieren, die richtig jeden Algorithmus berechnen, so lange die Eingänge weniger sind als relativ große Grenzen. Die Grenzen können vergrößert werden, aber nur durch das Verwenden neuer Formeln. Andererseits, dreifach Exponential-ober hat zu einem Entscheidungsverfahren für die Presburger Arithmetik gebunden wurde von Oppen (1978) bewiesen.

Anwendungen

Weil Presburger Arithmetik entscheidbarer, automatischer Lehrsatz provers für die Arithmetik von Presburger ist, bestehen. (Zum Beispiel zeigt der Probehelfer von Coq System eine Taktik für die Arithmetik von Presburger.) Macht die doppelte Exponentialkompliziertheit der Theorie es unausführbar, den Lehrsatz provers auf komplizierten Formeln zu verwenden, aber dieses Verhalten kommt nur in Gegenwart von verschachteltem quantifiers vor: Oppen und Nelson (1980) beschreiben einen automatischen Lehrsatz prover, der den Simplexalgorithmus auf einer verlängerten Arithmetik von Presburger ohne verschachtelten quantifiers verwendet. Der Simplexalgorithmus hat Exponentialgrenzfall-Laufzeit, aber zeigt beträchtlich bessere Leistungsfähigkeit für typische wahre Beispiele. Exponentiallaufzeit wird nur für besonders gebaute Fälle beobachtet. Das macht eine simplexbasierte Annäherung praktisch in einem Arbeitssystem.

Arithmetik von Presburger kann erweitert werden, um Multiplikation durch Konstanten einzuschließen, da Multiplikation wiederholte Hinzufügung ist. Die meisten Reihe-Subschrift-Berechnungen fallen dann innerhalb des Gebiets von entscheidbaren Problemen. Diese Annäherung ist die Basis von mindestens fünf Systemen des Beweises der Genauigkeit für Computerprogramme, mit dem Stanford Pascal Verifier gegen Ende der 1970er Jahre beginnend und obwohl zu Microsoft Spec# System von 2005 weitergehend.

Siehe auch

• Arithmetik von Robinson
• Küfer, D. C., 1972, "Lehrsatz, der Sich in der Arithmetik ohne Multiplikation" in B. Meltzer und D. Michie, Hrsg., Maschinenintelligenz Erweist. Edinburgher Universität Presse: 91-100.
• Ferrante, Jeanne und Charles W. Rackoff, 1979. Die Rechenbetonte Kompliziertheit von Logischen Theorien. Vortrag-Zeichen in der Mathematik 718. Springer-Verlag.
• Fischer, M. J. und Michael O. Rabin, 1974, ""Superexponentialkompliziertheit der Presburger Arithmetik." Verhandlungen des SIAM-AMS Symposiums in der Angewandten Mathematik Vol. 7: 27-41.
• Mojżesz Presburger, 1929, "sterben Über Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem sterben Hinzufügung als einzige Operation hervortritt" in Comptes Rendus du I congrès de Mathématiciens des Pays Slaves. Warszawa: 92-101.
• William Pugh, 1991, "Der Omega-Test: ein schneller und praktischer Programmieralgorithmus der ganzen Zahl für die Abhängigkeitsanalyse,".
• Reddy, C. R. und D. W. Loveland, 1978, "Presburger Arithmetik mit dem Begrenzten Quantifier Wechsel." ACM Symposium auf der Theorie der Computerwissenschaft: 320-325.
• Jung, P., 1985, "Lehrsätze von Godel, Exponentialschwierigkeit und Unentscheidbarkeit von arithmetischen Theorien: eine Ausstellung" in A. Nerode und R. Shore, Recursion Theorie, amerikanischer Mathematischer Gesellschaft: 503-522.
• Derek C. Oppen: 2 Ober Gebunden die Kompliziertheit der Presburger Arithmetik. J. Comput. System. Sci. 16 (3): 323-332 (1978)

Links

• Online-prover beweist Java applet oder widerlegt willkürliche Formeln der Arithmetik von Presburger (In Deutsch)
• http://www.philipp.ruemmer.org/princess.shtml Ein ganzer Lehrsatz Prover für die Presburger Arithmetik durch Philipp Rümmer