7.谓词演算.ppt

归结反演系统 (反驳) 归结反演系统：采用基于归结的反证法得到的定理证明系统。 例题： 已知前提： （1）能阅读的人是识字的 （2）海豚都不识字 （3）有些海豚是聪明的 求证：有些聪明的东西不会阅读 证明：用谓词形式表达所有前提以及结论。 ① R(x)： x 会阅读 ② L(x)： x 识字 ③ D(x)： x 是海豚字 ④ I(x)： x 是聪明的 ① ② ③ 结论： 利用公式标准化方法求出上式的S标准形，再写出对应的子句集 求证过程： ⑥ R(A) (4)，(5) 的归结式 ⑦ L (A) (1)，(6) 的归结式 ⑧ ~D (A) (2)，(7) 的归结式 ⑨ NIL (3)，(8) 的归结式 ① ② ③ ④ ⑤ 归结反演基本算法 问题：给定公式集S0，求证目标公式W成立。 基本方法：构造一个集合S0∪{~W}，如果该集合对于任何解释都是不可满足的 （归结出空子句），则S0→W成立。 基本算法： ① CLAUSES←S0∪{~W} ② Until NIL 是CLAUSES的成员， do： ③ begin ④ 在子句集CLAUSES中选择二个不同的可归结的子句 Ci, Cj ⑤ 计算Ci, Cj的归结式C ⑥ CLAUSES←将C加入到CLAUSES中 ⑦ end 说明：可归结子句的选择次序可以是任意的。 上面的例题用归结反演树表示如下： ① ② ③ ④ ⑤ 归结反演的控制策略 ① 宽度优先： ⑴ 首先归结出基本集S0∪{~W}所有可能的归结式（第一级归结） ⑵ 再同理归结出第二级归结式 ⑶ 依次类推，直到出现NIL子句 优点：具有完备性 不足：效率低，代价大 ② 支持集策略： 每次归结时，至少有一个选中的子句是目标的否定 ~W 或是 ~W 的后继节点。 讨论： ⑴ 支持集策略是完备的 ⑵ 它相当于带有约束条件的宽度优先策略 ⑶ 归结子句集的增长速度较宽度优先策略慢 ③ 单元子句优先策略： 每次归结时，优先选择单文字的子句（单元子句） 优点：所得到的归结式中的文字比与该单元子句进行归结的另一个子句中的文 字少 如： 单元子句 归结式 另一个子句 线性输入形策略： 基本原则：每个归结式至少有一个父节点属于基本集（即每次归结时，二个子句中至少有一个子句来自于初始集合S0∪{~W} ） 特点：不具备完备性，有些存在反演的系统不一定存在线性输入反演。 说明：因为每个归结式的父节点中至少有一个是基本集成员，所以NIL的父节点 也必有一个父节点来自基本集。 ⑤ 祖先过滤策略： 基本原则：每个归结式有一个父辈既可以在基本集中，也可以是另一个父辈的 祖先。 特点：与线性输入类似。它具有完备性。 A与C归结出D，其中A是C的父辈节点 ⑥ 策略的组合： 针对某些具体问题，综合运用上述若干策略。 如：支持集与线性输入形组合；支持集与祖先过滤组合等。 基于归结法的问答系统 问答系统要解决的问题形式： 有二种类型： 直接问答：求证当x=A时，W(A)成立。即：真假证明 间接问答：求证当x=？时，W(x)成立。即：求值证明 前面的证明方法都属于直接问答。间接问答方法需要采用构造方法。 提取问答方法 例题：① 如果Peter去哪儿，则Fido就去那儿 ② 如果Peter在学校 问题： Fido就去那儿？ 解：用谓词公式表达所有前提以及结论。 ① ② 结论： 子句