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

::L₁∨L₂∨...∨L_n

:を節と呼ぶ。

:ヒルベルトとその学生アッケルマンがその共著「記号論理学の基礎（Grundzüge der theoretischen Logik）」において定義したように、命題論理において、公理である前提の節 A₁ , A₂ , ... , A_m から節 D が導出可能であるとは、

::(A₁∧A₂∧...∧A_m) → D

はリテラルからなる選言命題でありホーン節は文字どおり節である。

</ref>。ホーン節が恒真であれば、当然原子命題 D は導出可能である。

=== 導出原理（resolvent principle） ===

''導出''とは二つの[[節]]より新しい節を導き出す操作で、一方の節に含まれるリテラル <math>l</math> と、他方の節に含まれる否定リテラル <math>\neg l</math> をのぞき、その他のリテラルの[[論理和]]をとることで、新しい節を得ることをいう。