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

述語論理式 ''P'' が[[恒真式|恒真]]であるかを証明する一般的な手続きは存在しないが、1930年に発表された[[エルブランの定理]]は[[エルブランの定理#エルブラン領域|エルブラン領域]]の要素を論理式に代入して命題論理のレベルに落としその充足不能性を調べることで、<math>\lnot P</math> が充足不能（恒偽）であれば有限のステップで証明できることを保証している。また、エルブランの論文には[[単一化]]アルゴリズムなど他のさまざまなものが含まれていた<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>。

 

 

プラウィツ（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>。