计算机科学家逻辑/谓词逻辑/消解策略/线性消解

线性消解

与我们为命题消解提供的基于饱和的过程形成对比，我们现在将讨论一种允许目标导向生成消解式的策略。我们稍后会看到，即在 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$