「導出原理」の版間の差分
削除された内容 追加された内容
I.hidekazu (会話 | 投稿記録) |
I.hidekazu (会話 | 投稿記録) |
||
17行目:
;節（clause）
:命題論理において原子命題を P とするとき、P または ¬P のことを'''リテラル'''（literal）と呼ぶ。リテラルの選言（disjunction）による結合命題を'''節'''（せつ、clause）と呼ぶ。例えば、L<sub>1</sub> , L<sub>2</sub> , ... , L<sub>n</sub> をリテラルとするときこの選言命題
::L<sub>1</sub> ∨ L<sub>2</sub> ∨ ... ∨ 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> ∧ A<sub>2</sub> ∧ ... ∧ A<sub>m</sub>) → D
:が恒真命題（tautology）であることを言うが、D が正のリテラル（原子命題）であるとき上記形式の複合命題を'''ホーン節'''（Horn clause）と呼ぶ<ref>
P → Q = ¬P∨Q と置き換えができることから
:(A<sub>1</sub> ∧ A<sub>2</sub> ∧ ... ∧ A<sub>m</sub>) → D
:= ¬(A<sub>1</sub> ∧ A<sub>2</sub> ∧... ∧ A<sub>m</sub>)∨D
:= ¬A<sub>1</sub> ∨ ¬A<sub>2</sub> ∨ ... ∨ ¬A<sub>m</sub>∨D
となる。A<sub>i</sub> は節（リテラルからなる選言命題）としたので、¬A<sub>i</sub> はリテラルからなる連言命題であり、
:¬A<sub>1</sub> ∨ ¬A<sub>2</sub> ∨ ... ∨ ¬A<sub>m</sub> ∨ D
はリテラルからなる選言命題でありホーン節は文字どおり節である。
</ref><ref>[[第五世代コンピュータ]]プロジェクトにおいて開発された並列論理型言語GHC（Guarded Horn Clauses；ガードされたホーン節）のHorn Clauses とはこのホーン節である。</ref>。ホーン節が恒真であれば、当然原子命題 D は導出可能である。
| |||