第5章基于谓词逻辑的机器推理详解.ppt

主讲：李 辉 Email：lihui@qust.edu.cn;序言;机器推理概述;机器推理概述;机器推理概述;第5章 基于谓词逻辑的机器推理 ;5.1.1谓词、函数、量词（1）;5.1.1谓词、函数、量词（2）;5.1.1谓词、函数、量词（3）;5.1.1谓词、函数、量词（4）;5.1.1谓词、函数、量词（5）;5.1.1谓词、函数、量词（5）;5.1.1谓词、函数、量词（6）;5.1.1谓词、函数、量词（7）;5.1.1谓词、函数、量词（8）;5.1.1谓词、函数、量词（9）;5.1.2 谓词公式 ;从原子谓词公式出发，通过命题联结词和量词，可以组成复合谓词公式。下面给出谓词公式的严格定义，即谓词公式的生成规则。;5.1.2 谓词公式 ;5.1.2 谓词公式 ;5.1.2 谓词公式 ;5.1.2 谓词公式 ;5.1.2 谓词公式 ;5.1.2 谓词公式 ;5.1.2 谓词公式 ;5.1.2 谓词公式 ;5.1.2 谓词公式 ;5.1.2 谓词公式 ;5.1.2 谓词公式 ;5.1.2 谓词公式 ;5.1.2 谓词公式 ; 5.1.3 谓词逻辑中的形式演绎推理;常用逻辑等价式(1);常用逻辑等价式(2) ;常用逻辑等价式(3) ;常用逻辑等价式(4);常用逻辑蕴含式(1);常用逻辑蕴含式(2); 5.1.3 谓词逻辑中的形式演绎推理; 5.1.3 谓词逻辑中的形式演绎推理; 5.1.3 谓词逻辑中的形式演绎推理;5.2 归结演绎推理-5.2.1子句集(1);5.2.1子句集(2);5.2.1子句集(3);5.2.1子句集(4);5.2.1子句集(5);5.2.1子句集(6);5.2.1子句集(7);5.2.1子句集(8);5.2.1子句集(9);5.2.1子句集(10);5.2.1子句集(11);5.2.1子句集(12);5.2.1子句集(13);5.2.1子句集(14);5.2.1子句集(15);5.2.1子句集(16);5.2.1子句集(17);5.2.1子句集(18);5.2.1子句集(19);5.2.1子句集(20);5.2.1子句集;5.2.1子句集;5.2.1子句集(21);5.2.2 命题逻辑中的归结原理(1);　　定义4 设L为一个文字，则称L与乛L为互补文字。 定义5 设C1,C2是命题逻辑中的两个子句，C1中有文字L1，C2中有文字L2，且L1与L2互补，从C1,C2中分别删除L1,L2，再将剩余部分析取起来，记构成的新子句为C12，则称C12为C1,C2的归结式(或消解式)，C1,C2称为其归结式的亲本子句， L1,L2称为消解基。 例5.9 设C1=乛P∨Q∨R,C2=乛Q∨S,于是C1,C2的归结式为 乛P∨R∨S;5.2.2 命题逻辑中的归结原理(3);例5.10 用归结原理验证分离规则和拒取式 A∧(A→B) ＝＞ B (A→B)∧﹁ B ＝＞﹁ A 解 A∧(A→B) ＝ A???(﹁ A∨B) ＝＞ B (A→B)∧﹁ B ＝ (﹁ A∨B)∧(﹁ B) ＝＞ ﹁ A ;类似的可以验证其他推理规则。这说明，归结原理可以代替其他所有的推理规则，而且推理步骤比较机械，为机器推理提供了方便。 由归结原理可知 ：L ∧ ? L ＝NIL 另外我们知道：L ∧ ? L ＝F（假）， 也就是 NIL F ;补充：;利用归结原理证明命题公式的思路 先求出要证明的命题公式的否定式的子句集S； 然后对子句集S（一次或者多次）使用归结原理； 若在某一步推出了空子句，即推出了矛盾，则说明子句集S是不可满足的，从而原否定式也是不可满足的，进而说明原公式是永真的。 ;推出空子句就说明子句集不可满足，原因是： 空子句就是F，推出空子句就是推出了F。 归结原理是正确的推理形式，由正确的推理形式推出了F，则说明前提不真，即归结出空子句的两个亲本子句至少有一个为假。 而这两个亲本子句如果都是原子句集S中的子句则S不可满足。 如果这两个亲本子句不是或不全是S中的子句，那么它们必定是某次归结的结果。 同样的道理向上回溯，一定会推出原子句集中至少有一个子句为假，从而说明S不可满足。;5.2.2 命题逻辑中的归结原理(8);例5.12 设公理集：P, (P?Q) ?R, (S?T) ?Q, T 求证：R ;子句集： (1) P (2) ?P??Q?R (3) ?S?Q (4) ?T?Q (5) T (6) ?R（目标求反）;例5.11 证明子句集