Presburger aritmetik
Presburger aritmetik är en första ordningens teori som beskriver naturliga tal med addition , men till skillnad från Peano aritmetik utesluter den påståenden om multiplikation . Uppkallad efter den polske matematikern Mojžeš Presburger , som 1929 föreslog motsvarande system av axiom i första ordningens logik , och även visade dess lösbarhet .
Axiom
Presburgers räknespråk inkluderar konstanterna 0, 1, en operation + och likhetspredikatet =. Axiomen ser ut så här:
- ¬ (0= x +1)
- x + 1 = y + 1 → x = y
- x + 0 = x
- ( x + y ) + 1 = x + ( y + 1)
- ( P (0) ∧ ( P ( x ) → P ( x + 1))) → P ( y ), där P är en första ordningens formel inklusive 0, 1, +, = och en fri variabel x .
Det bör noteras att (5) faktiskt inte är ett enda axiom, utan ett axiomschema som representerar en oändlig uppsättning axiom, ett för varje formel P . (5) är en formalisering av principen om matematisk induktion . Det kan inte på motsvarande sätt ersättas av något ändligt system av axiom. Således Presburger aritmetik är inte finitely axiomatizable .
Se även
Litteratur
- Cooper, DC, 1972, "Theorem Proving in Arithmetic without Multiplication" i B. Meltzer och D. Michie, red., Machine Intelligence . Edinburgh University Press: 91-100.
- Ferrante, Jeanne och Charles W. Rackoff, 1979. The Computational Complexity of Logical Theories . Lecture Notes in Mathematics 718. Springer-Verlag .
- Fischer, MJ och Michael O. Rabin , 1974, "Super-Exponential Complexity of Presburger Arithmetic. " Proceedings of the SIAM-AMS Symposium in Applied Mathematics Vol. 7 : 27-41.
- G. Nelson och DC Oppen. "En förenklare baserad på effektiva beslutsalgoritmer" // Proc . 5:e ACM SIGACT-SIGPLAN-symposiet om principer för programmeringsspråk: tidskrift. — apr. 1978. - S. 141-150 .
- Mojżesz Presburger , 1929, "Öber die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition as einzige Operation hervortritt" i Comptes Rendus du I congrès de Mathématiciens des Pays Slaves . Warszawa: 92-101.
- Pugh, William, 1991, " Omega-testet: en snabb och praktisk heltalsprogrammeringsalgoritm för beroendeanalys ",.
- Reddy, CR och DW Loveland, 1978, " Presburger Arithmetic with Bounded Quantifier Alternation. » ACM Symposium on Theory of Computing : 320-325.
- Vereshchagin, Shen. Föreläsningar om matematisk logik och teori om algoritmer. — MTsNMO, 2002.
Länkar