「導出原理」の版間の差分

m
編集の要約なし
m
述語論理式 ''P'' が[[恒真式|恒真]]であるかを証明する一般的な手続きは存在しないが、1930年に発表された[[エルブランの定理]]は[[エルブランの定理#エルブラン領域|エルブラン領域]]の要素を論理式に代入して命題論理のレベルに落としその充足不能性を調べることで、''¬P'' が充足不能(恒偽)であれば有限のステップで証明できることを保証している。また、エルブランの論文には[[単一化]]アルゴリズムなど他の様々なものが含まれていた<ref name=Buss1995>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.</ref>。
 
1950年代以降、計算機上での定理証明の研究が活発になり、[[ギルモアのアルゴリズム]](1960)や[[デービス・パトナムのアルゴリズム]](1958,1960) が考案された。デービス・パトナムのアルゴリズムには[[乗法標準形|連言標準形]]の使用や導出規則の考え方が含まれていた。しかし、これらはエルブランの定理の証明を直接計算機上で実現したような方法で、[[エルブランの定理#エルブラン領域|エルブラン領域]]の要素を順次生成して変数を含まない論理式(''基礎例'')を作成し命題論理のレベルで充足不能性を調べるものだったため、不要な論理式が多数生成され、非常に効率が悪かった<ref name=Davis2001>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</ref>。
 
プラウィツ(Dag Prawitz)は、論理式を生成してからチェックするのではなく、選言標準形に変換した論理式への適当な代入([[単一化]])によって充足不能性を調べる方法を1960年に提案した<ref name=Bibel2007>Wolfgang Bibel. ''Early History and Perspectives of Automated Deduction''. in ''Advances in Artificial Intelligence'', Lecture Notes in Computer Science, Springer-Verlag Berlin, 2007. ISBN 9783540745648</ref>。
7,353

回編集