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

→‎定義: ホーン節の定義をホーン節の項目に移動させた。
(参考文献の補足、節の入れ替え)
(→‎定義: ホーン節の定義をホーン節の項目に移動させた。)
 
== 定義 ==
=== ホーン節(Horn clause) ===
;節(clause)
:命題論理において原子命題を P とするとき、P または &not;P のことを'''リテラル'''(literal)と呼ぶ。リテラルの選言(disjunction)による結合命題を'''節'''(せつ、clause)と呼ぶ。例えば、L<sub>1</sub> , L<sub>2</sub> , ... , L<sub>n</sub> をリテラルとするときこの選言命題
::L<sub>1</sub> &or; L<sub>2</sub> &or; ... &or; L<sub>n</sub>
:を節と呼ぶ。
;ホーン節(Horn clause)
:ヒルベルトとその学生アッケルマンがその共著「記号論理学の基礎(Grundzüge der theoretischen Logik)」において定義したように、命題論理において、公理である前提の節 A<sub>1</sub> , A<sub>2</sub> , ... , A<sub>m</sub> から節 D が導出可能であるとは、
::(A<sub>1</sub> &and; A<sub>2</sub> &and; ... &and; A<sub>m</sub>) → D
:が恒真命題(tautology)であることを言うが、D が正のリテラル(原子命題)であるとき上記形式の複合命題を'''ホーン節'''(Horn clause)と呼ぶ<ref>
P → Q = &not;P&or;Q と置き換えができることから
:(A<sub>1</sub> &and; A<sub>2</sub> &and; ... &and; A<sub>m</sub>) → D
:= &not;(A<sub>1</sub> &and; A<sub>2</sub> &and;... &and; A<sub>m</sub>)&or;D
:= &not;A<sub>1</sub> &or; &not;A<sub>2</sub> &or; ... &or; &not;A<sub>m</sub>&or;D
となる。A<sub>i</sub> は節(リテラルからなる選言命題)としたので、&not;A<sub>i</sub> はリテラルからなる連言命題であり、
:&not;A<sub>1</sub> &or; &not;A<sub>2</sub> &or; ... &or; &not;A<sub>m</sub> &or; D
はリテラルからなる選言命題でありホーン節は文字どおり節である。
</ref><ref>[[第五世代コンピュータ]]プロジェクトにおいて開発された並列論理型言語GHC(Guarded Horn Clauses;ガードされたホーン節)のHorn Clauses とはこのホーン節である。</ref>。ホーン節が恒真であれば、当然原子命題 D は導出可能である。
{{details | ホーン節 }}
 
=== 導出原理(resolvent principle) ===
''導出''とは二つの[[節]]より新しい節を導き出す操作で、一方の節に含まれるリテラル <math>l</math> と、他方の節に含まれる否定リテラル <math>\neg l</math> をのぞき、その他のリテラルの[[論理和]]をとることで、新しい節を得ることをいう。