精选课件第四章逻辑推理.ppt

6．祖先过滤策略 这种策略与线性输入策略有点相似，但是，放宽了对子句的限制。每次参加归结的两个亲本子句，只要满足以下两个条件中的任意一个就可进行归结： （l）两个亲本子句中至少有一个是初始子句集中的子句； （2）如果两个亲本子句都不是初始子句集中的子句，则一个子句应该是另一个子句的先辈子句。所谓一个子句C1是另一个子句C2的先辈子句是指C2是由C1与别的子句归结后得到的归结式。 例： 设有如下子句集： S=｛┐Q（x）∨┐P（x），Q（y）∨┐P（y），┐Q（w）∨P（w），Q（a）∨P（a）｝ 用祖先过滤策略证明S为不可满足。 证明：从S出发，按祖先过滤策略归结过程如下图所示。 ┐Q(x) ∨┐P(x) Q(y) ∨┐P(y) ┐P(x) ┐Q(w) ∨P(w) ┐Q(w) Q(a) ∨P(a) P(a) NIL 可以证明祖先过滤策略也是完备的。 上面分别讨论了几种基本的归结策略，但在实际应用中，还可以把几种策略结合起来使用。至于如何结合，须根据具体需要而定。总之，在选择归结反演策略时，主要应考虑其完备性和效率问题。 线性输入策略的归结 * 使用某些前提产生结论的行动。 完备 * * 尽管使用删除策略的归结,少做了归结但不影响产生空子句。就是说使用删除策略的归结推理是完备的 2. 子句集的化简 在谓词逻辑中，任何一个谓词公式都可以通过应用等价关系及推理规则化成相应的子句集。其化简步骤如下： （l）消去连接词“→”和“←→” 反复使用如下等价公式： P →Q= P V Q P ←→Q= (P →Q) ∧(Q →P) = (P ∧ Q)V( P ∧ Q） 即可消去谓词公式中的连接词“→”和“←→ ”。 例如公式 ( x)(( y)P(x,y) → ( y )(Q(x,y) → R(x,y)))经等价变化后为 ( x)( ( y)P(x,y) V ( y )( Q(x,y) V R(x,y))) （2）减少否定符号的辖域（即把否定符号移到紧靠谓词的位置上） 反复使用双重否定律 ( P) == P 狄·摩根定律 （P∨Q）== P∧ Q （P∧Q）== P∨ Q  量词转换律 ( x）P==（彐x） P ， （彐x）P==（ x） P 将每个否定符号“ ”移到仅靠谓词的位置，使得每个否定符号最多只作用于一个谓词上。 例如，上步所得公式经本步变换后为 ( x)((彐y) P(x,y) ∨ (彐y )( Q(x,y) ∧ R(x,y))) （3）对变元标准化 在一个量词的辖域内，把谓词公式中受该量词约束的变元全部用另外一个没有出现过的任意变元代替，使不同量词约束的变元有不同的名字。 例如，上步所得公式经本步变换后为 ( x)((彐y) P(x,y) ∨ (彐z )( Q(x,z) ∧ R(x,z))) （4）化为前束范式 化为前束范式的方法是把所有量词都移到公式的左边，并且在移动时不能改变其相对顺序。由于第（3）步已对变元进行了标准化，每个量词都有自己的变元，这就消除了任何由变元引起冲突的可能，因此这种移动是可行的。 例如，上步所得公式化为前束范式后为: ( x) (彐y) (彐z )( P(x,y) ∨ ( Q(x,z) ∧ R(x,z))) （5）消去存在量词 消去存在量词时，需要区分以下两种情况。 若存在量词不出现在全称量词的辖域内（即它的左边没有全称量词），只要用一个新的个 体常量替换受该存在量词约束的变元，就可消去该存在量词。 若存在量词位于一个或多个全称量词的辖域内，例如 ( x1)( x2)……( xn)(彐y)P(x1,x2,……,xn,y) 则需要用 Skolem函数