Presburger Aritmetika

A Presburger aritmetika  egy elsőrendű elmélet , amely a természetes számokat összeadással írja le , de a Peano aritmetikával ellentétben kizárja a szorzásra vonatkozó állításokat . Mojžeš Presburger lengyel matematikusról nevezték el , aki 1929-ben javasolta a megfelelő axiómarendszert az elsőrendű logikában , és megmutatta annak megoldhatóságát is .

Axiómák

A Presburger aritmetikai nyelv tartalmazza a 0, 1 konstansokat, egy műveletet + és az egyenlőség predikátumot =. Az axiómák így néznek ki:

1. ¬ (0 = x +1)
2. x + 1 = y + 1 → x = y
3. x + 0 = x
4. ( x + y ) + 1 = x + ( y + 1)
5. ( P (0) ∧ ( P ( x )→ P ( x + 1))) → P ( y ), ahol P  egy elsőrendű képlet , amely 0, 1, +, = és egy x szabad változót tartalmaz .

Meg kell jegyezni, hogy (5) valójában nem egyetlen axióma, hanem egy axióma séma , amely végtelen axiómahalmazt reprezentál, minden P képlethez egyet . (5) a matematikai indukció elvének formalizálása . Egyenértékűen nem helyettesíthető semmilyen véges axiómarendszerrel. Így a Presburger aritmetika nem teljesen axiomatizálható .

Lásd még

• Peano aritmetika
• Robinson aritmetika
• Elsőrendű logika

Irodalom

• Cooper, DC, 1972, "Tételbizonyítás az aritmetikában szorzás nélkül", B. Meltzer és D. Michie, szerk., Machine Intelligence . Edinburgh University Press: 91-100.
• Ferrante, Jeanne és Charles W. Rackoff, 1979. The Computational Complexity of Logical Theories . Előadásjegyzetek matematikából 718. Springer-Verlag .
• Fischer, MJ és 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 és DC Oppen. "Egy hatékony döntési algoritmusokon alapuló egyszerűsítő"   // Proc . 5. ACM SIGACT-SIGPLAN szimpózium a programozási nyelvek alapelveiről: folyóirat. — ápr. 1978. - 141-150 .
• Mojżesz Presburger , 1929, „Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt” in Comptes Rendus du I congrès de Mathématiciens des Pays Slaves . Varsó: 92-101.
• Pugh, William, 1991, " Az Omega-teszt: gyors és praktikus egészszámú programozási algoritmus függőségi elemzéshez ".
• Reddy, CR és DW Loveland, 1978, Presburger Aritmetika határos kvantor váltakozással. » ACM Számítástechnikai Szimpózium : 320-325.

• Verescsagin, Shen. Előadások a matematikai logikáról és az algoritmusok elméletéről. – MTsNMO, 2002.

Linkek

• Az Online-Proofer Java egy olyan kisalkalmazás , amely ellenőrzi a Presburger aritmetikai képletek igazságtartalmát.  (Német)