|
===================================== 〔語彙分解〕的な部分一致の検索結果は以下の通りです。 ・ 導出 ： [どうしゅつ] (n,vs) derivation ・ 出 ： [で] 1. (n,n-suf) outflow 2. coming (going) out 3. graduate (of) 4. rising (of the sun or moon) 5. one's turn to appear on stage ・ 原 ： [はら, もと] 1. (n,n-suf,n-t) (1) origin 2. basis 3. foundation ・ 原理 ： [げんり] 【名詞】 1. principle 2. theory 3. fundamental truth ・ 理 ： [り] 【名詞】 1. reason
導出原理（どうしゅつげんり、）とは、により1965年に提案された〔J. Alan Robinson, ''A Machine-Oriented Logic Based on the Resolution Principle''. JACM, Volume 12, Issue 1, pp. 23–41. 1965.〕原理または手法を言う。 導出原理を元とする導出の手法は、その後の定理自動証明に大きな影響を与え、またPrologなどの論理プログラミング言語の基礎となった。 == 背景 == 述語論理式 ''P'' が恒真であるかを証明する一般的な手続きは存在しないが、1930年に発表されたエルブランの定理はエルブラン領域の要素を論理式に代入して命題論理のレベルに落としその充足不能性を調べることで、''¬P'' が充足不能（恒偽）であれば有限のステップで証明できることを保証している。また、エルブランの論文には単一化アルゴリズムなど他の様々なものが含まれていた〔Buss, Samuel R., "On Herbrand's Theorem", in Maurice, Daniel; Leivant, Raphaël, Logic and Computational Complexity, Lecture Notes in Computer Science, Springer-Verlag, pp. 195–209. 1995.〕。 1950年代以降、計算機上での定理証明の研究が活発になり、ギルモアのアルゴリズム(1960)やデービス・パトナムのアルゴリズム(1958,1960) が考案された。デービス・パトナムのアルゴリズムには連言標準形の使用や導出規則の考え方が含まれていた。しかし、これらはエルブランの定理の証明を直接計算機上で実現したような方法で、エルブラン領域の要素を順次生成して変数を含まない論理式(''基礎例'')を作成し命題論理のレベルで充足不能性を調べるものだったため、不要な論理式が多数生成され、非常に効率が悪かった〔Martin Davis. ''The Early History of Automated Deduction''. in ''Handbook of Automated Reasoning'', Volume I, Alan J.A. Robinson and Andrei Voronkov(ed), 2001. ISBN 9780444829498〕。 プラウィツ（Dag Prawitz）は、論理式を生成してからチェックするのではなく、選言標準形に変換した論理式への適当な代入（単一化）によって充足不能性を調べる方法を1960年に提案した〔Wolfgang Bibel. ''Early History and Perspectives of Automated Deduction''. in ''Advances in Artificial Intelligence'', 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「導出原理」の詳細全文を読む スポンサード リンク
|