4.1.3 含有变量的消解式

4.1.3 含有变量的消解式
为了对含有变量的子句使用消解规则，我们必须找到一个置换，作用于父辈子句使其含有互补文字。令父辈子句由｛L_i｝和｛M_i｝给出，而且假设这两个子句中的变量已经分离标准化。设｛l_i｝是｛L_i｝的一个子集，｛m_i｝是｛M_i｝的一个子集，使得集｛l_i｝和｛～m_i｝的并集存在一个最一般的合一者σ。消解两个子句｛L_i｝和｛M_i｝，得到的新子句.

{{L_i}-{l_i}}σ∪{{M_i}-{m_i}}σ

就是这两个子句的消解式。
消解两个子句时，可能有一个以上的消解式，因为有多种选择｛l_i｝和｛m_i｝的方法。不过，在任何情况下，它们最多具有有限个消解式。
作为例子，我们考虑两个子句:

P[x,f(A)]∨P[x,f(y)]∨Q(y) 和～P[z,f(A)]∨～Q(z)

如果取

{l_i}={P[x,f(A)]}，

{m_i}={～P[z,f(A)]}

那么得到消解式:

P[z,f(y)]∨～Q(z)∨Q(y)

如果取

{l_i}={Q(y)}，

{m_i}={～Q(z)}

那么得到消解式:

P[x,f(A)]∨P[x,f(y)]∨～P[y,f(A)]

进一步消解得消解式为:

P[y,f(y)]

可见这两个子句消解一共可得4个不同的消解式，其中3个是消解P得到的，而另一个是由消解Q得到的。

下面举几个对含有变量的子句使用消解的例子。

例1	例2

例3

表4.1 消解推理常用规则
父辈子句	消解式
P和～P∨Q（即P＝>Q)	Q
P∨Q和～P∨Q	Q
P∨Q和P∨～Q	Q∨～Q和P∨～P
～P∨P	NIL
～P∨Q（即P＝>Q）和～Q∨R（即Q＝>R）	～P∨R（即P＝>R）
B(x)和～B(x)∨C(x)	C(x)
P(x)∨Q(x)和～Q(f(y))	P(f(y)σ=｛f(y)/x｝
P(x,f(y))∨Q(x)∨R(f(a),y)和～P(f(f(a)),z)∨R(z,w)	Q(f(f(a)))∨R(f(a),y)∨R(f(y),w) σ=｛f(f(a))/x,f(y)/z｝

点击这里，可进行任意两个子句的消解推理 ……