自動定理証明

自動定理証明（じどうていりしょうめい、英: automated theorem proving, ATP）とは、自動推論 (AR) の中でも最も成功している分野であり、コンピュータプログラムによって数学的定理に対する証明を発見すること。ベースとなる論理によって、定理の妥当性を決定する問題は簡単なものから不可能なものまで様々である。

歴史

論理学的背景

論理学の起源はアリストテレスまで遡るが、現代的数理論理学は19世紀末から20世紀初頭に発展した。フレーゲの『概念記法』(1879) が完全な命題論理と一階述語論理の基本的なものを導入^[1]。同じくフレーゲの『算術の基礎』(1884)^[2]でも、形式論理の数学（の一部）を説明している。この流れを受け継いだのがラッセルとホワイトヘッドの『プリンキピア・マテマティカ』で、初版は1910年から1913年に出版され^[3]、1927年に第2版が出ている^[4]。ラッセルとホワイトヘッドは、公理と形式論理の推論規則からあらゆる数学的真理が導き出せると考え、証明自動化への道を拓いた。1920年、トアルフ・スコーレムはレオポールト・レーヴェンハイム（英語版）の成果を単純化したレーヴェンハイム-スコーレムの定理をもたらし、1930年にはエルブラン領域とエルブラン解釈により、一階の論理式の充足（不）可能性（および定理の妥当性）を命題論理の充足可能性問題に還元できることが示された^[5]。

1929年、Mojżesz Presburger はプレスブルガー算術（加法と等号のある自然数の理論）が決定可能であり、その言語内の任意の文の真偽を判定できるアルゴリズムを示した^[6]^[7]。しかしその直後、クルト・ゲーデルが Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I (1931) を発表し、十分に強力な公理系はその体系内で証明も反証もできない文を含みうることを示した。1930年代にこの課題を研究したのがアロンゾ・チャーチとアラン・チューリングで、それぞれ独自に等価な計算可能性の定義を与え、決定不能な具体例も示した。

最初の実装

第二次世界大戦後、第一世代のコンピュータが登場。1954年、マーチン・デービス（英語版）がプリンストン高等研究所にて真空管コンピュータJOHNNIAC（英語版）上にプレスブルガーのアルゴリズムを実装した。デービスによれば「2つの偶数の総和も偶数であることを証明するという大きな成果があった」という^[7]^[8]。さらに野心的な試みとして Logic Theorist がある。これはアレン・ニューウェルとハーバート・サイモンとクリフ・ショーが開発したもので、『プリンキピア・マテマティカ』の命題論理を対象とした推論システムだった。こちらもJOHANNIAC上で動作し、命題論理の少数の公理と推論規則（モーダスポネンス、命題変数の置換など）から証明を構築した。ヒューリスティックによる誘導を使っており、『プリンキピア・マテマティカ』の52の定理のうち38の証明に成功した^[7]。

Logic Theoristのヒューリスティックとは人間の数学者のエミュレートを試みることであり、妥当な定理すべてについて証明できることを保証できなかった。対照的に、より体系的なアルゴリズムで（少なくとも理論上は）一階述語論理の完全性を達成できている。初期の手法ではエルブランとスコーレムの成果に基づき、一階述語論理の論理式を複数の命題論理の論理式に変換していた。そして、いくつかの技法で命題論理式の充足不可能性をチェックする。ギルモアのアルゴリズムは加法標準形に変換することで充足可能性を判定しやすくしていた^[7]^[9]。

問題の決定可能性

使用する論理によって、論理式の妥当性の判定は自明なものから不可能なものまで様々である。命題論理の多くの問題では、定理は決定可能だがco-NP完全問題であり、汎用的な証明には指数時間アルゴリズムしかないと考えられている。一階述語論理では、完全性定理より妥当な論理式は証明可能であり、その逆も成り立つから、妥当な論理式の全体は再帰的に枚挙可能である。したがって、妥当な論理式の証明を機械的に探索することはできる。

妥当でない文、すなわち与えられた定理から意味論的に導かれない式は認識可能とは限らない。さらにゲーデルの不完全性定理によれば、ある程度の算術を含む無矛盾な体系は本質的不完全であり、本質的不完全な体系は本質的決定不可能であるから、とくに決定不可能である。そのような場合、一階述語論理の定理証明機は証明探索の完了に失敗する（停止しない）可能性がある。このような理論上の制限はあるが、実用的な定理証明機は様々な難しい問題の証明をすることができる。

産業への応用

産業分野での応用例としては、LSIの設計とその検証が挙げられ、モデル的手法とともに使われている。Pentium FDIV バグ以来、FPUの設計は極めて厳密に行われている。AMDやインテルはプロセッサの設計検証に自動定理証明を使っている。

一階述語論理の定理証明

一階述語論理の定理証明は自動定理証明の中でも最も研究が進んでいる。この論理は適度に自然で直感的な方法で様々な問題を記述できる程度に表現豊かである。一方、半決定的で健全で完全な計算方法が開発されており、完全自動システムを構築することが可能である。さらに表現力のある論理（高階述語論理や様相論理）は、さらに様々な問題を記述可能だが、それらの定理証明は一階述語論理ほど開発が進んでいない。

ベンチマークと競技会

実装システムの品質は標準ベンチマーク例の大きなライブラリ Thousands of Problems for Theorem Provers (TPTP) の存在によって高められている^[12]。また、Conference on Automated Deduction(CADE) 主催の ATP System Competition (CASC) は一階述語論理システムの競技会であり、これもシステムの品質向上に寄与している。

以下に主なシステムを列挙する（いずれも少なくとも1回は CASC で優勝している）。

E は Purely Equational Calculus に基づいた高性能証明機。ミュンヘン工科大学の自動推論グループが開発した。
Otter はアルゴンヌ国立研究所で開発された世界で初めて広く使われた高性能証明機である。導出と導出における統合推論に基づいている。Otterの後継としてProver9とMasce4がある。
SETHEO はゴール指向の model elimination 法に基づいた高性能システム。ミュンヘン工科大学の自動推論グループが開発した。E と SETHEO は統合され、E-SETHEO となった。
Vampire はマンチェスター大学の Andrei Voronkov と Krystof Hoder が開発・実装した。かつては Alexandre Riazanov も参加していた。定理証明機のワールドカップ（the CADE ATP System Competition）の最高の CNF (MIX) 部門で7年間優勝している（1999年、2001～2006年）。
Waldmeister は unit-equational な一階述語論理に特化したシステムである。10年間にわたって CASC UEQ 部門で優勝している（1997年～2006年）。
SPASSは等号を含む一階述語論理の定理証明機である。マックス・プランク研究所が開発した。

主な技法

比較

名称	ライセンス	ウェブサービス	ライブラリ	スタンドアロン	バージョン	最新	作者	備考
ACL2	GPL v2	No	No	Yes	5.0	2012-8-23	Matt Kaufmann, J. Strother Moore	-
Prover9 / Mace4	GPLv2	No	Yes	Yes	v05	2009-11-04/	William McCune / アルゴンヌ国立研究所	-
Otter	パブリックドメイン	System on TPTPを使用	Yes	No	3.3f	2004-9	William McCune / Argonne National Laboratory	Prover9 / Mace4 が後継
j'Imp	?	No	No	Yes	-	2010-5-28	André Platzer	-
Metis	?	No	Yes	No	2.2	2010-5-24	Joe Hurd	-
Jape	?	Yes	Yes	No	1.0	2010-3-22	Adolfo Gustavo Neto, USP	-
PVS	?	No	Yes	No	4.2	2008-7	SRIインターナショナル	-
Leo II	?	System on TPTPを使用	Yes	Yes	1.2.8	2011	Christoph Benzmüller, Frank Theiss, Larry Paulson. ベルリン自由大学とケンブリッジ大学	-
EQP	?	No	Yes	No	0.9e	2009-5	William McCune / アルゴンヌ国立研究所	-
SAD	?	Yes	Yes	No	2.3-2.5	2008-8-27	Alexander Lyaletski, Konstantin Verchinine, Andrei Paskevich	-
PhoX	?	No	Yes	No	0.88.100524	-	Christophe Raffalli, Philippe Curmin, Pascal Manoury, Paul Roziere	-
KeYmaera	GPL	Java Web Startを使用	Yes	Yes	2.1	2012-5	André Platzer, Jan-David Quesel; Philipp Rümmer; David Renshaw	-
Gandalf	?	No	Yes	No	3.6	2009	Matt Kaufmann, J. Strother Moore, テキサス大学オースティン校	-
Tau	?	No	Yes	No	-	2005	Jay R. Halcomb, Randall R. Schulz, H&S Information Systems	-
E	GPL	System on TPTPを使用	No	Yes	E 1.4	2011-8-20	Stephan Schulz, ミュンヘン工科大学	-
SNARK	Mozilla Public License	No	Yes	No	snark-20080805r018b	2008	Mark E. Stickel	-
Vampire	?	System on TPTPを使用	Yes	Yes	Third re-incarnation Vampire	2011	Andrei Voronkov, Alexandre Riazanov, Krystof Hoder	-
Waldmeister	?	Yes	Yes	No	-	-	Thomas Hillenbrand, Bernd Löchner, Arnim Buch, Roland Vogt, Doris Diedrich	-
Saturate	?	No	Yes	No	2.5	1996-10	Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela	-
Theorem Proving System (TPS)	?	No	Yes	No	-	2004-6-24	カーネギーメロン大学	-
SPASS	?	Yes	Yes	Yes	3.7	2005-11	マックス・プランク研究所	-
IsaPlanner	GPL	No	Yes	Yes	IsaPlanner 2	2007	Lucas Dixon, Johansson Moa	-
KeY	GPL	Yes	Yes	Yes	1.6	2010-10	カールスルーエ大学, チャルマース工科大学, コブレンツ大学	-
Theorem Checker	?	Yes	No	No	0	2010	Robert J. Swartz, 北イリノイ大学	-
Princess	GPL	Java Web StartとSystem on TPTPを使用	Yes	Yes	2012-11-02	2012	Philipp Rümmer, ウプサラ大学	-

フリーソフトウェア

プロプライエタリ

脚注

[脚注の使い方]

^ Frege, Gottlob (1879). Begriffsschrift. Verlag Louis Neuert
^ Frege, Gottlob (1884). Die Grundlagen der Arithmetik. Breslau: Wilhelm Kobner
^ Bertrand Russell; Alfred North Whitehead (1910-1913). Principia Mathematica (1st ed.). Cambridge University Press
^ Bertrand Russell; Alfred North Whitehead (1927). Principia Mathematica (2nd ed.). Cambridge University Press
^ Herbrand, Jaques (1930). Recherches sur la théorie de la démonstration
^ Presburger, Mojżesz (1929). “Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt”. Comptes Rendus du I congrès de Mathématiciens des Pays Slaves (Warszawa): 92–101.
^ ^a ^b ^c ^d Davis, Martin (2001), “The Early History of Automated Deduction”, in Robinson, Alan; Voronkov, Andrei, Handbook of Automated Reasoning, 1, Elsevier )
^ Bibel, Wolfgang (2007). “Early History and Perspectives of Automated Deduction”. KI 2007. LNAI (Springer) (4667): 2–18 2012年9月2日閲覧。.
^ Gilmore, Paul (1960). “A proof procedure for quantification theory: its justification and realisation”. IBM Journal of Research and Development 4: 28–35.
^ W.W. McCune (1997). “Solution of the Robbins Problem”. Journal of Automated Reasoning 19 (3).
^ Gina Kolata (December 10, 1996). “Computer Math Proof Shows Reasoning Power”. The New York Times 2008年10月11日閲覧。
^ Sutcliffe, Geoff. “The TPTP Problem Library for Automated Theorem Proving”. 2012年9月8日閲覧。
^ “SRI International Computer Science Laboratory - John Rushby”. SRI International. 22 September 2012閲覧。

参考文献

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 ed.). McGraw-Hill
Alan Robinson and Andrei Voronkov (eds.), ed (2001). Handbook of Automated Reasoning Volume I & II. Elsevier and MIT Press
Fitting, Melvin (1996). First Order and Automated Theorem Proving (2nd ed.). Springer. http://comet.lehman.cuny.edu/fitting/

外部リンク

[1] Frege, Gottlob (1879). Begriffsschrift. Verlag Louis Neuert

[2] Frege, Gottlob (1884). Die Grundlagen der Arithmetik. Breslau: Wilhelm Kobner

[3] Bertrand Russell; Alfred North Whitehead (1910-1913). Principia Mathematica (1st ed.). Cambridge University Press

[4] Bertrand Russell; Alfred North Whitehead (1927). Principia Mathematica (2nd ed.). Cambridge University Press

[5] Herbrand, Jaques (1930). Recherches sur la théorie de la démonstration

[6] Presburger, Mojżesz (1929). “Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt”. Comptes Rendus du I congrès de Mathématiciens des Pays Slaves (Warszawa): 92–101.

[Davis2001-7] Davis, Martin (2001), “The Early History of Automated Deduction”, in Robinson, Alan; Voronkov, Andrei, Handbook of Automated Reasoning, 1, Elsevier )

[Bibel2007-8] Bibel, Wolfgang (2007). “Early History and Perspectives of Automated Deduction”. KI 2007. LNAI (Springer) (4667): 2–18 2012年9月2日閲覧。.

[9] Gilmore, Paul (1960). “A proof procedure for quantification theory: its justification and realisation”. IBM Journal of Research and Development 4: 28–35.

[10] W.W. McCune (1997). “Solution of the Robbins Problem”. Journal of Automated Reasoning 19 (3).

[11] Gina Kolata (December 10, 1996). “Computer Math Proof Shows Reasoning Power”. The New York Times 2008年10月11日閲覧。

[12] Sutcliffe, Geoff. “The TPTP Problem Library for Automated Theorem Proving”. 2012年9月8日閲覧。

[13] “SRI International Computer Science Laboratory - John Rushby”. SRI International. 22 September 2012閲覧。

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]