自動定理証明

自動定理証明

自動定理証明（Automated Theorem Proving, ATP）は、自動推論の中でも特に発展した分野であり、コンピュータプログラムを用いて数学的定理の証明を自動的に行う技術です。定理の妥当性を判定する問題は、使用する論理体系によって難易度が大きく異なります。

歴史的背景

自動定理証明の歴史は、数理論理学の発展と深く関わっています。アリストテレスにまで遡る論理学の起源ですが、現代的な数理論理学は19世紀末から20世紀初頭にかけて発展しました。フレーゲの『概念記法』(1879) は、完全な命題論理と一階述語論理の基礎を導入し、ラッセルとホワイトヘッドの『プリンキピア・マテマティカ』は、公理と形式論理の推論規則からすべての数学的真理が導き出せると考え、証明の自動化への道を開きました。

1920年、トアルフ・スコーレムはレーヴェンハイム-スコーレムの定理を単純化し、1930年にはエルブラン領域とエルブラン解釈によって、一階の論理式の充足（不）可能性を命題論理の充足可能性問題に還元できることを示しました。1929年には、Mojżesz Presburgerがプレスブルガー算術の決定可能性を示しましたが、その直後、ゲーデルの不完全性定理が発表され、十分に強力な公理系はその体系内で証明も反証もできない文を含みうることを示しました。

初期の試み

第二次世界大戦後、初期のコンピュータが登場すると、自動定理証明の実装が始まりました。1954年、マーチン・デービスがJOHNNIAC上にプレスブルガーのアルゴリズムを実装し、Logic Theoristが開発されました。Logic Theoristは、『プリンキピア・マテマティカ』の命題論理を対象とした推論システムで、ヒューリスティックを用いて52の定理のうち38の証明に成功しました。

初期の手法は、エルブランとスコーレムの成果に基づき、一階述語論理の論理式を複数の命題論理の論理式に変換し、命題論理式の充足不可能性をチェックしていました。

問題の決定可能性

論理式の妥当性の判定は、使用する論理によって異なります。命題論理では決定可能ですがco-NP完全問題であり、一階述語論理では、妥当な論理式の全体は再帰的に枚挙可能です。しかし、ゲーデルの不完全性定理によれば、ある程度の算術を含む無矛盾な体系は本質的に不完全であり、決定不可能です。

関連する問題

自動定理証明に関連する問題として、自動証明検証や証明のコンピュータによる支援があります。自動定理証明で生成される証明は長大になることが多く、証明の圧縮が重要となります。対話型定理証明機では、ユーザーがシステムにヒントを与え、証明を支援します。

定理証明は、公理から出発して推論規則に従って推論を行うものであり、モデル検査などの他の技術とは異なります。ただし、モデル検査的手法を推論規則として利用するハイブリッド型の定理証明システムも存在します。

産業への応用

自動定理証明は、LSIの設計・検証などの産業分野でも応用されています。Pentium FDIV バグ以降、FPUの設計は厳密に行われており、AMDやインテルはプロセッサの設計検証に自動定理証明を使用しています。

一階述語論理の定理証明

一階述語論理の定理証明は、自動定理証明の中でも最も研究が進んでいます。この論理は、様々な問題を記述できる程度に表現豊かであり、完全自動システムを構築することが可能です。

ベンチマークと競技会

自動定理証明システムの品質は、TPTPなどの標準ベンチマーク例や、CADE主催のATP System Competition (CASC) によって高められています。

主な技法

自動定理証明で用いられる主な技法には、導出とユニフィケーション、項書き換え、モデル検査、数学的帰納法、二分決定図、DPLLアルゴリズム、分析的タブロー法などがあります。

関連人物

自動定理証明の分野には、ジャック・エルブラン、Woody Bledsoe、Robert S. Boyer、Alan Bundy、William McCuneなど、多くの著名な研究者が存在します。

自動定理証明は、理論的な研究から産業応用まで、幅広い分野で重要な役割を果たしています。

もう一度検索