計算機科學家邏輯/謂詞邏輯/消解策略/線性消解

線性消解

與我們為命題消解提供的基於飽和的過程形成對比，我們現在將討論一種允許目標導向生成消解式的策略。我們稍後會看到，即在 Horn 子句的情況下，這種線性策略是邏輯程式解釋的基礎。

給定一組子句 $S$ 和 $S$ 中的子句 $C_{0}$ 。頂子句 $C_{0}$ 的線性推導是一個序列 $C_{0},C_{1},\cdots ,C_{n}$ ，其中 $\forall 1\leq i\leq n$ $C_{i}$ 是 $C_{i-1}$ 和 $B$ 的消解式，其中 $B\in S\cup \{C_{j}\mid j<i\}$ 。如果 $C_{n}=\square$ ，則該序列稱為線性反駁。

定義 25

下面是一個線性推導的例子。子句集 $S$ 由以下給出

{\begin{matrix}symptom(s)&(1)\\cause(c_{1})\lor cause(c_{2})\lor \lnot symptom(s)&(2)\\treatment(t_{0})\lor \lnot cause(c_{1})&(3)\\treatment(t_{1})\lor \lnot cause(c_{1})&(4)\\treatment(t_{0})\lor \lnot cause(c_{2})&(5)\\treatment(t_{2})\lor \lnot cause(c_{2})&(6)\\\end{matrix}}

並結合目標 $\lnot treatment(x)$ ，我們得到以下反駁，其中來自 $S$ 的子句由相應的數字給出： $\lnot treatment(X)$ ，(4)， $\lnot cause(c_{1})$ ，(2)， $cause(c_{2})\lor \lnot symptom(s)$ ，(1)， $cause(c_{2})$ ，(6)， $treatment(t_{2})$ ， $\square$