22037k4.jpgアルゴンヌ国立研究所は1960年代以降2000年代まで、自動定理証明のリーダーだった。中でも最も成功している分野であり、コンピュータプログラムによって数学的定理に対する証明を発見すること。ベースとなる論理によって、定理の妥当性を決定する問題は簡単なものから不可能なものまで様々である。19世紀末から20世紀初頭に発展した。完全な命題論理と一階述語論理の基本的なものを導入[1]。フレーゲの『算術の基礎』(1884)[2]でも、形式論理の数学(の一部)を説明している。この流れを受け継いだのがラッセルとホワイトヘッドの『プリンキピア・マテマティカ』で、初版は1910年から1913年に出版され[3]、1927年に第2版が出ている[4]。ラッセルとホワイトヘッドは、公理と形式論理の推論規則からあらゆる数学的真理が導き出せると考え、証明自動化への道を拓いた。1920年、トアルフ・スコーレムはレオポールト・レーヴェンハイム(English版)の成果を単純化したレーヴェンハイム-スコーレムの定理をもたらし、1930年にはエルブラン領域とエルブラン解釈により、一階の論理式の充足(不)可能性(および定理の妥当性)を命題論理の充足可能性問題に還元できることが示された[5]。プレスブルガー算術(English版)(加法と等号のある自然数の理論)が決定可能であり、その言語内の任意の文の真偽を判定できるアルゴリズムを示した[6][7]。発表し、十分に強力な公理系はその体系内で証明も反証もできない文を含みうることを示した。1930年代にこの課題を研究したのがアロンゾ・チャーチとアラン・チューリングで、それぞれ独自に等価な計算可能性の定義を与え、決定不能な具体例も示した。1954年、マーチン・デービス(English版)がプリンストン高等研究所にて真空管コンピュータJOHNNIAC(English版)上にプレスブルガーのアルゴリズムを実装した。デービスによれば「2つの偶数の総和も偶数であることを証明するという大きな成果があった」という[7][8]。これはアレン・ニューウェルとハーバート・サイモンとクリフ・ショーが開発したもので、『プリンキピア・マテマティカ』の命題論理を対象とした推論システムだった。こちらもJOHANNIAC上で動作し、命題論理の少数の公理と推論規則(モーダスポネンス、命題変数の置換など)から証明を構築した。ヒューリスティックによる誘導を使っており、『プリンキピア・マテマティカ』の52の定理のうち38の証明に成功した[7]。ヒューリスティックとは人間の数学者のエミュレートを試みることであり、妥当な定理すべてについて証明できることを保証できなかった。対照的に、より体系的なアルゴリズムで(少なくとも理論上は)一階述語論理の完全性を達成できている。初期の手法ではエルブランとスコーレムの成果に基づき、一階述語論理の論理式を複数の命題論理の論理式に変換していた。いくつかの技法で命題論理式の充足不可能性をチェックする。ギルモアのアルゴリズムは加法標準形に変換することで充足可能性を判定しやすくしていた[7][9]。使用する論理によって、論理式の妥当性の判定は自明なものから不可能なものまで様々である。命題論理の多くの問題では、定理は決定可能だがco-NP完全問題であり、汎用的な証明には指数時間アルゴリズムしかないと考えられている。一階述語論理では、完全性定理より妥当な論理式は証明可能であり、その逆も成り立つから、妥当な論理式の全体は再帰的に枚挙可能である。したがって、妥当な論理式の証明を機械的に探索することはできる。妥当でない文、すなわち与えられた定理から意味論的に導かれない式は認識可能とは限らない。ゲーデルの不完全性定理によれば、ある程度の算術を含む無矛盾な体系は本質的不完全であり、本質的不完全な体系は本質的決定不可能であるから、とくに決定不可能である。定理証明機は証明探索の完了に失敗する(停止しない)可能性がある。このような理論上の制限はあるが、実用的な定理証明機は様々な難しい問題の証明をすることができる。関連した問題に、自動証明検証と、証明のコンピュータによる支援がある。定理の証明の正当性を検証するには、証明の各段階を原始再帰関数やプログラムで検証できる必要があり、そうすることで問題は常に決定可能となる。人間のユーザーがシステムにヒントを与える必要がある。自動化の度合いによっては、証明機が単なる証明検証機的なものとなってユーザーが提供した形式的証明を検証するだけの場合もあるし、大部分の証明を自動的に行う場合もある。対話型証明機は様々なタスクに使えるが、完全自動システムは長期にわたって人間の数学者がてこずってきた困難な問題を証明してきた[10][11]。そのような成功例は稀で、一般に困難な問題を解くには熟練したユーザーの補助が必要である。定理証明とそれ以外の区別の観点として、公理から出発して推論規則に従って推論を行い、いわゆる証明を行うものを定理証明と呼ぶ。モデル検査などのそれ以外の技術では、考えられる全ての状態を列挙するようなものである(モデル検査の実装ではもう少し賢さが必要であるが、それで力づくの手法でなくなるわけではない)。モデル検査的手法を推論規則として利用するハイブリッド型の定理証明システムも存在する。特定の定理を証明するために書かれたプログラムも存在し、プログラムがある結果を返して終了したときに定理が真であることが証明される。そのようなプログラムの好例として四色定理の計算機支援証明がある。人間の手では証明できなかった問題を証明したことで物議をかもしたそのプログラムは、非常に複雑で検証不可能と言われた。他の例として重力付き四目並べゲームで先手が必ず勝つことを証明したことが挙げられる。産業分野での応用例としては、LSIの設計とその検証が挙げられ、モデル的手法とともに使われている。以来、FPUの設計は極めて厳密に行われている。AMDやインテルはプロセッサの設計検証に自動定理証明を使っている。定理証明は自動定理証明の中でも最も研究が進んでいる。この論理は適度に自然で直感的な方法で様々な問題を記述できる程度に表現豊かである。半決定的で健全で完全な計算方法が開発されており、完全自動システムを構築することが可能である。表現力のある論理(高階述語論理や様相論理)は、さらに様々な問題を記述可能だが、それらの定理証明は一階述語論理ほど開発が進んでいない。存在によって高められている[12]。一階述語論理システムの競技会であり、これもシステムの品質向上に寄与している。基づいた高性能証明機。ミュンヘン工科大学の自動推論グループが開発した。アルゴンヌ国立研究所で開発された世界で初めて広く使われた高性能証明機である。導出と導出における統合推論に基づいている。Otterの後継としてen:Prover9Prover9とMasce4がある。法に基づいた高性能システム。ミュンヘン工科大学の自動推論グループが開発した。