< 上一个 | 内容 | 下一个 >

2.2.4 归结原理

2.2.4.1 基子句的归结原理

对任意两个基子句 C1 和 C2，如果 C1 中存在文字 L1，C2 中存在文字 L2，且 L1=L2，则从 C1，C2 中分别删除 L1，L2，将 C1，C2 的剩余部分析取起来构成子句，称为 C1 和 C2 的归结式。例如， C1=PQR，C2=QS，于是 C1 和 C2 的归结式为PRS。设 C1， C2 是两个基子句，则 C1，C2 的归结式C 是 C1 和 C2 的逻辑结果。

设 S 是子句集，从 S 推出子句 C 的演绎是有限子句序列： C1,C2,...,Ck。其中Ci或者是S 中子句，或者是Cj和Cr的归结式（j<i,r<i）；并且 Ck=C。从 S 推出空子句的演绎称为反驳，或称为 S 的一个证明。从子句集S 演绎出子句C，是指存在一个从 S 推出C 的演绎。

例 2，S={PQ,PQ,PQ,PQ}

（1）PQ；

（2）PQ；

（3）PQ；

（4）PQ；

（5）Q 由（1）,（2）；

（6）Q 由（3）,（4）；

（7） 由（5）,（6）。

如果基子句集 S 是不可满足的，则存在从 S 推出空子句的归结演绎。

2.2.4.2 一般子句的归结原理

提升引理：如果 C1’和 C2’分别是子句 C1 和 C2 的例，C’是 C1’和 C2’的归结式，则存在 C1 和 C2 的一个归结式 C，使 C’是 C 的例。根据 Herbrand 定理和提升引理，可以证明一阶逻辑中归结原理的完备性：若子句集 S 是不可满足的，则存在从 S 推出空子句的归结演绎。

例 3：已知某些病人喜欢所有的医生，没有一个病人喜欢任意一个骗子。证明任意一个医生都不是骗子。

证：令 P(x): x 是病人

D(x): x 是医生

Q(x): x 是骗子

L(x,y): x 喜欢 y

A1: x(P(x)y(D(y)L(x,y)))

A2: x(P(x)y(Q(y)L(x,y))) B: x(D(x)Q(x))

要证明公式 A1A2B 是不可满足的，先求出其 Skolem 范式中的子句集：

A1=xy(P(x)(D(y)L(x,y)))，

Skolem 范式为 y(P(a)(D(y)L(a,y)))

A2 = xy(P(x)Q(y)L(x,y))，Skolem 范式与前束范式相同

B = x(D(x)Q(x)) ，Skolem 范式为D(b)Q(b)

因此，A1A2B 公式的子句集为下述（1）-（5）

（1）P(a)；

（2）D(y)L(a,y)；

（3）P(x)Q(y)L(x,y)；

（4）D(b)；

（5）Q(b)；

（6）L(a,b) 由（2），（4）；

（7）Q(y)L(a,y) 由（1），（4）；

（8）L(a,b) 由（5），（7）；

（9） 由（6），（8）。

2.2.4.3 删除策略

归结原理是比 Gilmore 或 Herbrand 方法更有效的判定一阶逻辑

中公式的不可满足性的方法。但是，归结原理的效率，也由于在归结过程中产生大量的无用子句而受到影响。在子句集 S 上使用归结原理的最直接的一种方法是，计算 S 中所有子句对的归结式，并将这些归结式并入S，再进一步计算所有子句对的归结式。重复此过程，直到空子句被导出。这个过程被称为水平浸透法。对前面例子中子句集 S={PQ,PQ,PQ,PQ}使用水平浸透法，将生成非常多的对导出空子句无用的子句。

为了解决防止多余子句产生这个问题，提高归结推理效率，删除策略被引入。

称子句C 包含子句D，当且仅当存在替换 σ 使得CσD。D 称为被包含子句。例如，设C=P(x), D=P(a)Q(a)，令σ={a/x}，则Cσ=P(a)D，即 C 包含 D。

设 S 是子句集，下面的序列是从 S 出发推出子句 C 的演绎 D： C1,C2,...,Ck(=C)。如果 Ci 是重言式，或者 Ci 被某个Cj 包含（j<i），则将 Ci 从这个演绎中删除，称对此演绎 D 实行了删除策略。删除策略是完备的，即，设 S 是不可满足子句集，如果在水平浸透法中使用删除策略，则最后仍可以推导出空子句。

< 上一个 | 内容 | 下一个 >