自動定理証明
出典: フリー百科事典『ウィキペディア（Wikipedia）』
自動定理証明（Automated Theorem Proving、ATP）とは、自動推論(AR) の中でも最も成功している分野であり、コンピュータプログラムによって数学的定理を証明すること。ベースとなる論理によって、定理の妥当性を決定する問題は簡単なものから不可能なものまで様々である。
目次 |
[編集] 概要
命題論理の多くの問題では、定理は決定可能だがNP完全問題であり、汎用的な証明には指数時間アルゴリズムしかないと考えられている。一階述語論理では、定理の識別は再帰的に枚挙可能である。すなわち、無限のリソースを前提とすれば、任意の有効な定理を証明できる。無効な文、すなわち与えられた定理から導けない式は認識可能とは限らない。そのような場合、一階述語論理の定理証明機は証明探索の完了に失敗する可能性がある。このような理論上の制限はあるが、実用的な定理証明機は様々な難しい問題の証明をすることができる。
やや単純だが関連した問題として証明の検証がある。ある定理の証明の正当性を如何にして検証するか、である。そのためには、証明の各段階を原始再帰関数やプログラムで検証できる必要があり、そうすることで問題は常に決定可能となる。
対話型定理証明機では人間のユーザーがシステムにヒントを与える必要がある。自動化の度合いによっては、証明機が単なる証明検証機的なものとなってユーザーが提供した形式的証明を検証するだけの場合もあるし、大部分の証明を自動的に行う場合もある。対話型証明機は様々なタスクに使えるが、完全自動システムは長期にわたって人間の数学者がてこずってきた困難な問題を証明してきた。しかし、そのような成功例は稀で、一般に困難な問題を解くには熟練したユーザーの補助が必要である。
定理証明とそれ以外の区別の観点として、公理から出発して推論規則に従って推論を行い、いわゆる証明を行うものを定理証明と呼ぶ。モデル検査などのそれ以外の技術では、考えられる全ての状態を列挙するようなものである（モデル検査の実装ではもう少し賢さが必要であるが、それで力づくの手法でなくなるわけではない）。モデル検査的手法を推論規則として利用するハイブリッド型の定理証明システムも存在する。また、特定の定理を証明するために書かれたプログラムも存在し、プログラムがある結果を返して終了したときに定理が真であることが証明される。そのようなプログラムの好例として四色定理の計算機支援証明がある。人間の手では証明できなかった問題を証明したことで物議をかもしたそのプログラムは、非常に複雑で検証不可能と言われた。他の例として Connect Four ゲームで先手が必ず勝つことを証明したことが挙げられる。
自動定理証明は主に集積回路の設計と検証で商業利用されている。PentiumのFDIV命令バグ問題以降、最近のマイクロプロセッサの複雑なFPU部分の設計には細心の注意が払われている。AMD、インテルその他の企業では定理証明によって回路の動作を検証しているのである。
[編集] 一階述語論理の定理証明
一階述語論理の定理証明は自動定理証明の中でも最も研究が進んでいる。この論理は適度に自然で直感的な方法で様々な問題を記述できる程度に表現豊かである。一方、半決定的で健全で完全な計算方法が開発されており、完全自動システムを構築することが可能である。さらに表現力のある論理（高階述語論理や様相論理）は、さらに様々な問題を記述可能だが、それらの定理証明は一階述語論理ほど開発が進んでいない。実装システムの品質は標準ベンチマーク例の大きなライブラリ(TPTP)の存在によって高められる。また、Conference on Automated Deduction(CADE) 主催の ATP System Competition (CASC) は一階述語論理システムの競技会であり、これもシステムの品質向上に寄与している。
以下に主なシステムを列挙する（いずれも少なくとも1回は CASC で優勝している）。
- E は Purely Equational Calculus に基づいた高性能証明機。ミュンヘン工科大学の自動推論グループが開発した。
- Otter はアルゴンヌ国立研究所で開発された世界で初めて広く使われた高性能証明機である。導出と導出における統合推論に基づいている。
- SETHEO はゴール指向のModel Elimination法に基づいた高性能システム。ミュンヘン工科大学の自動推論グループが開発した。E と SETHEO は統合され、E-SETHEO となった。
- Vampire はマンチェスター大学の Andrei Voronkov が開発・実装した。かつては Alexandre Riazanov も参加していた。定理証明機のワールドカップ（the CADE ATP System Competition）の最高の CNF (MIX) 部門で7年間優勝している（1999年、2001～2006年）。
- Waldmeister は unit-equational な一階述語論理に特化したシステムである。10年間にわたって CASC UEQ 部門で優勝している（1997年～2006年）。
[編集] 主な技法
[編集] 実装例
- ACL2 theorem prover
- Carine theorem prover
- Coq
- CVC theorem prover
- Cycプロジェクト
- E equational theorem prover
- Isabelle theorem prover
- Gandalf theorem prover
- HOL theorem prover
- HOL Light theorem prover
- KIV
- LCF theorem prover
- LoTREC
- MetaPRL
- Matita proof assistant
- Mizar
- NuPRL
- Otter theorem prover
- Paradox theorem prover
- PhoX
- Prover Plug-In (市販品)
- ProverBox (市販品)
- Prototype Verification System
- SPARK プログラミング言語
- Tau theorem prover
- TPS (Theorem Proving System)
- Twelf
- Vampire theorem prover
これらの一部に関しては http://www.tptp.org/CASC/J2/SystemDescriptions.html または QPQ website に情報がある。http://www.tptp.org には一階述語論理の定理証明に関する情報がある。また、http://www.tptp.org/TSTP には解法に関する情報がある。
[編集] 関連著名人
- Woody Bledsoe、人工知能のパイオニア。
- Robert S. Boyer、ボイヤー-ムーア定理証明機の開発者の1人。1999年ハーブランド賞を共同受賞。
- William McCune アルゴンヌ国立研究所。初期の高性能自動定理証明機 Otter 開発者の1人。2000年 ハーブランド賞受賞。
- Martin Davis、"Handbook of Artificial Reasoning" の著者。DPLLアルゴリズムの開発者の1人。2005年ハーブランド賞受賞。
- Branden Fitelson カリフォルニア大学バークレー校。
- Michael Genesereth、スタンフォード大学教授。
- Michael J. C. Gordon は HOL theorem prover 開発の責任者。
- Donald W. Loveland デューク大学。DPLL-procedure の開発者の1人。model eliminationの開発者。2001年 ハーブランド賞を受賞。
- Norman Megill、自動証明された定理に関するデータベース metamath.orgの管理人。
- J Strother Moore、ボイヤー-ムーア定理証明機の開発者の1人。1999年 ハーブランド賞を共同受賞。
- Ross Overbeek アルゴンヌ国立研究所。The Fellowship for Interpretation of Genomes を設立。
- Lawrence C. Paulson ケンブリッジ大学。高階論理システムの研究。Isabelle proof assistant の開発者の1人。
- John Rushby SRIインターナショナル。
- Geoff Sutcliffe マイアミ大学。TPTP collection の管理人、CADE コンテストの主催者。
- Robert Veroff ニューメキシコ大学。
- Andrei Voronkov Vampire の開発者にして "Handbook of Automated Reasoning" の共編者。
- Larry Wos アルゴンヌ国立研究所。
[編集] 参考文献
- Chin-Liang Chang; Richard Char-Tung Lee (1973年).Symbolic Logic and Mechanical Theorem Proving. Academic Press.
- Loveland, Donald W. (1978年).Automated Theorem Proving: A Logical Basis. Fundamental Studies in Computer Science Volume 6. North-Holland Publishing.
- Gallier, Jean H. (1986年).Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row Publishers.
- Duffy, David A. (1991年).Principles of Automated Theorem Proving. John Wiley & Sons.
- Wos, Larry; Overbeek, Ross; Lusk, Ewing; Boyle, Jim (1992年).Automated Reasoning: Introduction and Applications, 2nd edition, McGraw-Hill.
- (2001年) Alan Robinson and Andrei Voronkov (eds.)Handbook of Automated Reasoning Volume I & II. Elsevier and MIT Press.
- Fitting, Melvin (1996年).First Order and Automated Theorem Proving, 2nd edition, Springer.
[編集] 関連項目
- 計算機支援証明
- 形式的検証
- 証明複雑性
