In matemaattinen logiikka , aritmeettinen Presburger on teoria ensimmäisen kertaluvun on luonnollisten lukujen varustettu lisäksi . Sen esitteli Mojżesz Presburger vuonna 1929 . Tämä on Peano-aritmeettinen ilman kertolaskua , toisin sanoen vain lisäämällä nollan ja seuraajaoperaation lisäksi. Toisin kuin Peano-aritmeettinen, Presburgerin aritmeetti on päätettävissä . Tämä tarkoittaa, että on olemassa algoritmi, joka määrittää, onko ilmoitus kieli Presburger aritmeettinen on todistettavasti päässä aksioomista on Presburger aritmeettinen.
Allekirjoitus kielestä Presburger n aritmeettinen sisältää symbolit vakioiden 0 ja 1, binary toiminto symboli +. Aritmeettinen määritellään seuraavilla aksiomeilla:
(5) on induktiokaavio ja se on ääretön joukko aksiomia. Voimme osoittaa, että Presburgerin aritmeettista arvoa ei voida hienosäätää ensimmäisen asteen logiikassa.
Mojżesz Presburger osoitti vuonna 1929, että hänen johdonmukainen laskutoimitus on täydellinen . Koska rekursiivisesti aksiomatisoitava ja täydellinen aksiomaattinen teoria on ratkaistavissa , päätämme sellaisen algoritmin olemassaolon, joka päättää Presburgerin aritmeettisen kielen ehdotuksen perusteella, onko se todistettavissa vai ei.
Toisin kuin Presburgerin aritmeikka, Peanon aritmeikka ei ole täydellinen Gödelin epätäydellisyyslausekkeen alla . Peano n aritmeettinen ei ole ratkeava (katso päätös ongelma ).
Harkitse tässä seuraavaa päätösongelmaa : päättää, onko Presburgerin aritmeettinen kaava totta. Michael J. Fisher ja Michael O. Rabin ovat osoittaneet, että tällä päätösongelmalla on kaksinkertainen eksponentiaalinen sisäinen monimutkaisuus. Toisin sanoen, päätösongelma on 2EXPTIME-vaikea: se on yksi 2EXPTIME- kompleksisuusluokan vaikeimmista ongelmista , joka on kaksinkertaisen eksponentiaalisen ajallisesti ratkaistavan ongelman luokka.
On olemassa ei-elementaarinen päätöksentekomenettely, joka perustuu äärellisten automaattien teoriaan.
Oppen antoi vuonna 1978 kolminkertaisen eksponentiaalisen algoritmin, toisin sanoen, ongelma, onko Presburgerin aritmeettinen kaava totta, on 3EXPTIME-tilassa, joka on kolminkertaisen eksponentiaalisen ajan ratkaistavien ongelmien luokka.
Berman antoi vuonna 1980 tarkemman tuloksen monimutkaisuuden teoriasta vaihtelevia koneita käyttäen : Presburgerin aritmeetti on täydellinen ajoissa 2 2 n O (1) ja n vuorottelua varten määritetylle ongelmaluokalle , jossa luku n on tarkistettavan kaavan koko . Tämä luokka sisältää 2EXPTIME ja sisältyy 3EXPTIME.
SMT Z3 ratkaisija työkoneiden Presburger aritmeettinen. Coq todiste avustaja antaa omega strategiaa .
Peano aritmeettinen asetetaan kielen Presburger aritmeettinen sekä symboli x binaarinen funktio, jonka intuitiivinen tulkinta on kertolasku. Peanon aritmeettinen sisältää lisäaksiomeja. Aritmeettinen Robinson , se ei sisällä induktiohoitona.