Presburger arithmetic

Presburger arithmetic）中的命题是否为真的问题更加困难。Fischer和Rabin（英语：Michael O. Rabin）于1974年证明每个决定Presburger命题的真伪性的算法有最少22cn的运行时间，c为某个常数。这裡，n是Presburger

complexity theory）和光滑分析（smooth analysis）。实际中的例子包括Presburger arithmetic（英语：Presburger arithmetic）、布尔可满足性问题（参见SAT solver）和背包问题。 计算机科学主题 時間複雜度 遊戲複雜度 空间复杂度

}{\mbox{DTIME}}\left(2^{2^{n^{c}}}\right)} 眾所周知的雙重指數時間演算法包括： 預膨脹算術（英语：Presburger arithmetic）的決策程序 計算葛洛拿基底（英语：Gröbner basis）（在最差狀況） 實封閉體的量詞消去至少耗費雙重指數時間，而且可以在這樣的時間內完成。

求系统能将一些基本操作例如加法和乘法形式化，例如在鲁宾逊算术Q中那样。有一些更弱的公理系统是相容而且完备的，例如Presburger算術（英语：Presburger arithmetic），它包括所有的一阶逻辑的真命题和关于加法的真命题。 公理系统可能含有无穷条公理（例如皮亚诺算术就是这样），但要