「導出原理」の版間の差分
削除された内容 追加された内容
I.hidekazu (会話 | 投稿記録) |
I.hidekazu (会話 | 投稿記録) |
||
30行目:
:¬A<sub>1</sub>∨¬A<sub>2</sub>∨...∨¬A<sub>m</sub>∨D
はリテラルからなる選言命題でありホーン節は文字どおり節である。
</ref><ref>[[第五世代コンピュータ]]プロジェクトにおいて開発された並列論理型言語GHC（Guarded Horn Clauses；ガードされたホーン節）のHorn Clauses とはこのホーン節である。</ref>。ホーン節が恒真であれば、当然原子命題 D は導出可能である。
=== 導出原理（resolvent principle） ===
| |||