プレスバーガー算術

プレスバーガー算術(英: Presburger arithmetic)とは加法を含む自然数に関する一階述語論理体系である。 モイジェシュ・プレスバーガーにより1929年に導入された。 プレスバーガー算術のシグネチャには加法と等号のみが含まれ乗法は省かれる。 公理には数学的帰納法の公理図式を含む。

プレスバーガー算術は加法と乗法両方含むペアノ算術より弱い体系である。ペアノ算術とは異なりプレスバーガー算術は決定可能である。 これはプレスバーガー算術の言語で書かれた任意の閉論理式がプレスバーガー算術の公理で証明可能かどうかを判定するアルゴリズムが存在することを意味する。 この決定問題の計算複雑性は漸近的に二重指数関数であることがFischer & Rabin (1974)で示されている。

概説

プレスバーガー算術の言語は0と1、加法と解釈される二項関数+からなる。公理は以下の論理式を全称閉包したものである。

1. ¬(0 = x + 1)
2. x + 1 = y + 1 → x = y
3. x + 0 = x
4. x + (y + 1) = (x + y) + 1
5. P(x)をプレスバーガー算術の言語による自由変数xを含む一階述語論理式とする。このとき次の論理式は公理である。

(P(0) ∧ ∀x(P(x) → P(x + 1))) → ∀y P(y).

(5) は数学的帰納法の公理図式であり、無限個の公理を表している。 (5) は有限の公理で置き換えることができないためプレスバーガー算術は有限公理化不可能である。

プレスバーガー算術は因数分解に関する規則や素数のような概念を形式化できない。 一般的に乗法に関する自然数の概念は不完全性と決定不可能性につながることからプレスバーガー算術では定義することはできない。 しかし、個々の論理式としては形式化可能である。例えば次は証明可能である。"任意のxに対して、あるyが存在し : (y + y = x) ∨ (y + y + 1 = x)" これは、すべての自然数は偶数もしくは奇数のどちらかであることを意味する。

性質

モイジェシュ・プレスバーガーはプレスバーガー算術に関して以下を証明した。

• 無矛盾: 任意の文とその否定が共に演繹可能であることはない。
• 完全: 任意の文が演繹可能であるか、もしくはその否定が演繹可能である。
• 決定可能: 任意に与えられた文が定理であるか定理ではないかを判定するアルゴリズムが存在する。

関連項目

• ロビンソン算術

参考文献

• Cooper, D. C., 1972, "Theorem Proving in Arithmetic without Multiplication" in B. Meltzer and D. Michie, eds., Machine Intelligence Vol. 7. Edinburgh University Press: 91–99.
• Enderton, Herbert (2001). A mathematical introduction to logic (2nd ed.). Boston, MA: Academic Press. ISBN 978-0-12-238452-3 
• Ferrante, Jeanne, and Charles W. Rackoff, 1979. The Computational Complexity of Logical Theories. Lecture Notes in Mathematics 718. Springer-Verlag.
• Fischer, Michael J.; Rabin, Michael O. (1974). “Super-Exponential Complexity of Presburger Arithmetic”. Proceedings of the SIAM-AMS Symposium in Applied Mathematics 7: 27–41. http://www.lcs.mit.edu/publications/pubs/ps/MIT-LCS-TM-043.ps. 
• G. Nelson and D. C. Oppen (Apr 1978). “A simplifier based on efficient decision algorithms”. Proc. 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages: 141–150. doi:10.1145/512760.512775. 
• 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. Warszawa: 92–101. — see Stansifer (1984)for an English translation
• Ryan Stansifer (September 1984). Presburger's Article on Integer Arithmetic: Remarks and Translation (PDF) (Technical Report). Vol. TR84-639. Ithaca/NY: Dept. of Computer Science, Cornell University.
• William Pugh, 1991, "The Omega test: a fast and practical integer programming algorithm for dependence analysis,".
• Reddy, C. R., and D. W. Loveland, 1978, "Presburger Arithmetic with Bounded Quantifier Alternation." ACM Symposium on Theory of Computing: 320–325.
• Young, P., 1985, "Gödel theorems, exponential difficulty and undecidability of arithmetic theories: an exposition" in A. Nerode and R. Shore, Recursion Theory, American Mathematical Society: 503-522.
• Oppen, Derek C. (1978). “A 2^22pn Upper Bound on the Complexity of Presburger Arithmetic” (PDF). J. Comput. Syst. Sci. 16 (3): 323–332. doi:10.1016/0022-0000(78)90021-1. http://www.sciencedirect.com/science/article/pii/0022000078900211/pdf?md5=0415089a2d692fcece18b43b5f63c67d&pid=1-s2.0-0022000078900211-main.pdf. 
• Berman, L. (1980). “The Complexity of Logical Theories”. Theoretical Computer Science 11 (1): 71–77. doi:10.1016/0304-3975(80)90037-7. 
• Nipkow, T (2010). “Linear Quantifier Elimination”. Journal of Automated Reasoning 45 (2): 189–212. doi:10.1007/s10817-010-9183-0. 
• King, Tim; Barrett, Clark W.; Tinelli, Cesare (2014). “Leveraging linear and mixed integer programming for SMT”. FMCAD 2014: 139–146. doi:10.1109/FMCAD.2014.6987606. 

外部リンク

• online prover A Java applet proves or disproves arbitrary formulas of Presburger arithmetic (In German)
• [1] A complete Theorem Prover for Presburger Arithmetic by Philipp Rümmer