預報算術是自然數的壹階理論,加法,以榮譽Moj?eszPresburger為名,他在1929年介紹了它。Presburger算法的簽名只包含加法運算和相等,完全省略乘法運算。 公理包括歸納方案。
預飽和算術比Peano算術弱得多,包括加法運算和乘法運算。 與Peano算術不同,Presburger算術是壹個可判定的理論。 這意味著,對於Presburger算術語言中的任何句子,可以算法地確定該句子是否可以從Presburger算術的公理證明。 Fischer&Rabin(1974)所示,這個決策問題的漸近運行時運算復雜度是雙指數的。
Presburger arithmetic
Presburger arithmetic is the first-order theory of the natural numbers with addition, named in honor of Moj?esz Presburger, who introduced it in 1929. The signature of Presburger arithmetic contains only the addition operation and equality, omitting the multiplication operation entirely. The axioms include a schema of induction.
Presburger arithmetic is much weaker than Peano arithmetic, which includes both addition and multiplication operations. Unlike Peano arithmetic, Presburger arithmetic is a decidable theory. This means it is possible to algorithmically determine, for any sentence in the language of Presburger arithmetic, whether that sentence is provable from the axioms of Presburger arithmetic. The asymptotic running-time computational complexity of this decision problem is doubly exponential, however, as shown by Fischer & Rabin (1974).