最初の実装
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2018/05/28 07:09 UTC 版)
第二次世界大戦後、第一世代のコンピュータが登場。1954年、マーチン・デービス（英語版）がプリンストン高等研究所にて真空管コンピュータJOHNNIAC（英語版）上にプレスブルガーのアルゴリズムを実装した。デービスによれば「2つの偶数の総和も偶数であることを証明するという大きな成果があった」という。さらに野心的な試みとして Logic Theorist がある。これはアレン・ニューウェルとハーバート・サイモンとクリフ・ショーが開発したもので、『プリンキピア・マテマティカ』の命題論理を対象とした推論システムだった。こちらもJOHANNIAC上で動作し、命題論理の少数の公理と推論規則（モーダスポネンス、命題変数の置換など）から証明を構築した。ヒューリスティックによる誘導を使っており、『プリンキピア・マテマティカ』の52の定理のうち38の証明に成功した。 Logic Theorist のヒューリスティックとは人間の数学者のエミュレートを試みることであり、妥当な定理すべてについて証明できることを保証できなかった。対照的に、より体系的なアルゴリズムで（少なくとも理論上は）一階述語論理の完全性を達成できている。初期の手法ではエルブランとスコーレムの成果に基づき、一階述語論理の論理式を複数の命題論理の論理式に変換していた。そして、いくつかの技法で命題論理式の充足不可能性をチェックする。ギルモアのアルゴリズムは加法標準形に変換することで充足可能性を判定しやすくしていた。
※この「最初の実装」の解説は、「自動定理証明」の解説の一部です。
「最初の実装」を含む「自動定理証明」の記事については、「自動定理証明」の概要を参照ください。
- 最初の実装のページへのリンク
