最初の実装とは? わかりやすく解説

最初の実装

出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2018/05/28 07:09 UTC 版)

自動定理証明」の記事における「最初の実装」の解説

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

※この「最初の実装」の解説は、「自動定理証明」の解説の一部です。
「最初の実装」を含む「自動定理証明」の記事については、「自動定理証明」の概要を参照ください。

ウィキペディア小見出し辞書の「最初の実装」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。 お問い合わせ



英和和英テキスト翻訳>> Weblio翻訳
英語⇒日本語日本語⇒英語
  

辞書ショートカット

すべての辞書の索引

「最初の実装」の関連用語

最初の実装のお隣キーワード
検索ランキング

   

英語⇒日本語
日本語⇒英語
   



最初の実装のページの著作権
Weblio 辞書 情報提供元は 参加元一覧 にて確認できます。

   
ウィキペディアウィキペディア
Text is available under GNU Free Documentation License (GFDL).
Weblio辞書に掲載されている「ウィキペディア小見出し辞書」の記事は、Wikipediaの自動定理証明 (改訂履歴)の記事を複製、再配布したものにあたり、GNU Free Documentation Licenseというライセンスの下で提供されています。

©2025 GRAS Group, Inc.RSS