Gelen matematiksel mantık , aritmetik Presburger olan teori ilk düzenin içinde doğal sayılar ile sağlanan ek . 1929'da Mojżesz Presburger tarafından tanıtıldı . Bu, sıfıra ve ardıl işleme ek olarak , çarpma olmaksızın , yani yalnızca toplama ile Peano aritmetiğidir . Peano aritmetiğinin aksine, Presburger aritmetiği karar verilebilir . Bu , Presburger aritmetiğinin aksiyomlarından Presburger aritmetiğinin dilinin bir ifadesinin kanıtlanabilir olup olmadığını belirleyen bir algoritma olduğu anlamına gelir .
İmza Presburger en aritmetik dilinin sabitleri 0 ve 1 ikili işlev simgesi + sembollerini içerir. Aritmetik, aşağıdaki aksiyomlarla tanımlanır:
(5) tümevarım şemasıdır ve sonsuz bir aksiyom kümesidir. Presburger'in aritmetiğinin birinci dereceden mantıkta sonlu olarak aksiyomlaştırılamayacağını gösterebiliriz.
Mojżesz Presburger , 1929'da tutarlı olan aritmetiğinin tamamlandığını gösterdi . Bir itibariyle yinelemeli aksiyomatize ve tam aksiyomatik teori olduğunu Karar verilebilen , biz varlığını anlamak algoritma o kanıtlanabilir olup olmadığı, Presburger en aritmetik dilinde bir önerme verilen karar verir.
Presburger aritmetik aksine, Peano aritmetik altında tam değildir eksiklik teoremi arasında Gödel . Peano'nun aritmetiği karar verilemez (bkz. Karar problemi ).
Burada şu karar problemini düşünün : Presburger aritmetiğinin bir formülünün doğru olup olmadığına karar vermek. Michael J. Fisher ve Michael O. Rabin , bu karar probleminin iki kat üstel bir iç karmaşıklığa sahip olduğunu kanıtladılar. Diğer bir deyişle, karar problemi EXPTIME-zordur: 2EXPTIME karmaşıklık sınıfının en zor problemlerinden biridir, iki kat üstel zamanlı karar verilebilir problemler sınıfıdır.
Sonlu otomata teorisine dayanan temel olmayan bir karar prosedürü vardır.
Oppen 1978'de üçlü üslü bir algoritma verdi, yani Presburger'in aritmetiğinin bir formülünün doğru olup olmadığı sorunu, üçlü üslü zamanla karar verilebilir problemler sınıfı olan 3EXPTIME'de.
1980'de Berman, alternatif makineler kullanarak karmaşıklık teorisinin daha kesin bir sonucunu verdi : Presburger aritmetiği, zaman 2 2 n O (1) ve n dönüşümlerinde karar verilen problemler sınıfı için tamamlandı , burada n sayısı kontrol edilecek formülün boyutudur . Bu sınıf 2EXPTIME içerir ve 3EXPTIME içinde bulunur.
SMT Z3 çözücü uygular Presburger aritmetik. Coq kanıtı asistanı sağlar omega strateji .
Peano aritmetik Presburger aritmetik artı kimin sezgisel yorumlanması çarpma bir sembol × ikili işlevinin dile ayarlanmış. Peano'nun aritmetiği ek aksiyomlar içerir. Aritmetik Robinson , bu indüksiyon rejimi içermez.