Presburger Aritmetik
Presburger-aritmetik er en førsteordensteori, der beskriver naturlige tal med addition , men i modsætning til Peano-aritmetik udelukker den udsagn om multiplikation . Opkaldt efter den polske matematiker Mojžeš Presburger , som i 1929 foreslog det tilsvarende system af aksiomer i førsteordens logik , og også viste dets løselighed .
Aksiomer
Presburgers regnesprog inkluderer konstanterne 0, 1, én operation + og lighedsprædikatet =. Aksiomerne ser således ud:
- ¬ (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 ), hvor P er en førsteordens formel inklusive 0, 1, +, = og én fri variabel x .
Det skal bemærkes, at (5) faktisk ikke er et enkelt aksiom, men et aksiomskema, der repræsenterer et uendeligt sæt af aksiomer, et for hver formel P . (5) er en formalisering af princippet om matematisk induktion . Det kan ikke på tilsvarende måde erstattes af noget endeligt system af aksiomer. Således Presburger aritmetik er ikke endeligt aksiomatizable .
Se også
Litteratur
- Cooper, DC, 1972, "Theorem Proving in Arithmetic without Multiplication" i B. Meltzer og D. Michie, red., Machine Intelligence . Edinburgh University Press: 91-100.
- Ferrante, Jeanne , og Charles W. Rackoff, 1979. The Computational Complexity of Logical Theories . Forelæsningsnotater i matematik 718. Springer-Verlag .
- Fischer, MJ og 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 og DC Oppen. "En forenkling baseret på effektive beslutningsalgoritmer" // Proc . 5. ACM SIGACT-SIGPLAN symposium om principper for programmeringssprog: tidsskrift. – 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-testen: en hurtig og praktisk heltalsprogrammeringsalgoritme til afhængighedsanalyse ",.
- Reddy, CR og DW Loveland, 1978, " Presburger Arithmetic with Bounded Quantifier Alternation. » ACM Symposium on Theory of Computing : 320-325.
- Vereshchagin, Shen. Forelæsninger om matematisk logik og teori om algoritmer. — MTsNMO, 2002.
Links