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

→‎定義: ホーン節の定義を記載した。
(→‎定義: ホーン節の定義を記載した。)
 
== 定義 ==
=== ホーン節(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>
:を節と呼ぶ。
;ホーン節(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>。ホーン節が恒真であれば、当然原子命題 D は導出可能である。
=== 導出原理(resolvent principle) ===
''導出''とは二つの[[節]]より新しい節を導き出す操作で、一方の節に含まれるリテラル <math>l</math> と、他方の節に含まれる否定リテラル <math>\neg l</math> をのぞき、その他のリテラルの[[論理和]]をとることで、新しい節を得ることをいう。
 
導出は[[完全性|完全]]な証明系であることが知られている。
 
==== 例 === =
<math> p \to q </math> を節形式にすると <math> \lnot p \lor q </math> となる。<math> C_R </math> を<math> C_1, C_2 </math> の導出節とすると、[[モーダスポネンス|前件肯定]]は以下の導出と同じである。