人工智能谓词演算与归结原理.ppt

第三章 谓词演算与归结原理 一阶谓词演算是一种形式语言，具有严密的理论体系 是一种常用的知识表示方法 例： City（北京） City（上海） Age（张三，23） (?x)(? y)(? z)(F(x, y)?F(y, z)?GF(x, z)) 3.1 归结原理 归结原理是一种定理证明方法，1965年由Robinson提出，从理论上解决了定理证明问题。 子句集 无量词约束 元素只是文字的析取 否定符只作用于单个文字 元素间默认为合取 例：{~I(z)?R(z), I(A), ~R(x) ?L(x), ~D(y)} 化子句集的方法 例：(?z) (?x)(?y){[(P(x) ?Q(x)) ?R(y)] ?U(z)} 1, 消蕴涵符 理论根据：a ?b = ~a ?b (?z) (?x)(?y){[~(P(x) ?Q(x)) ? R(y)] ?U(z)} 2, 移动否定符 理论根据：~(a ?b) = ~a ?~b ~(a ?b) = ~a ?~b ~(?x)P(x)=(?x)~P(x) ~(?x)P(x)=(?x)~P(x) (?z) (?x)(?y){[(~P(x) ?~Q(x)) ? R(y)] ?U(z)} 化子句集的方法（续1） 3, 变量标准化 即：对于不同的约束，对应于不同的变量 (?x)A(x) ? (?x)B(x) = (?x)A(x) ? (?y)B(y) 4, 量词左移 (?x)A(x) ? (?y)B(y) = (?x) (?y) {A(x) ? B(y)} 5, 消存在量词 (skolem化） 原则：对于一个受存在量词约束的变量，如果他不受全程量词约束，则该变量用一个常量代替，如果他受全程量词约束，则该变量用一个函数代替。 (?z) (?x)(?y){[(~P(x) ?~Q(x)) ? R(y)] ?U(z)} = (?x) {[(~P(x) ?~Q(x)) ? R(f(x))] ?U(a)} 化子句集的方法（续2） 6, 化为合取范式 即(a?b) ? (c?d) ? (e?f)的形式 (?x){[(~P(x) ?~Q(x)) ? R(f(x))]?U(a)} = (?x){(~P(x) ?~Q(x)) ? R(f(x))?U(a)} = (?x){[~P(x) ? R(f(x))?U(a)] ? [~Q(x))? R(f(x))?U(a)]} 7, 隐去全称量词 {[~P(x) ? R(f(x))?U(a)] ?[~Q(x))? R(f(x))?U(a)]} 化子句集的方法（续3） 8, 表示为子句集 {~P(x) ? R(f(x))?U(a), ~Q(x))? R(f(x))?U(a)} 9, 变量标准化（变量换名） {~P(x1) ? R(f(x1))?U(a), ~Q(x2))? R(f(x2))?U(a)} 定理： 若S是合式公式F的子句集，则F永假的充要条件是S不可满足。 S不可满足：若nil?S，则S不可满足。 证明的思路： 目标的否定连同已知条件一起，化为子句集，并给出一种变换的方法，使得 S ?S1 ?S2 ?... ?Sn 同时保证当Sn不可满足时，有S不可满足。 3.2 归结方法（命题逻辑） 设子句： C1=L?C1’ C2=(~L) ?C2’ 则归结式C为： C=C1’ ?C2’ 定理： 子句集S={C1, C2, …, Cn}与子句集 S1={C, C1, C2, …, Cn}的不可满足性是等价的。其中，C是C1和C2的归结式。 归结的例子 设公理集： 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（目标求反） 子句集： (1) P (2) ~P?~Q?R (3) ~S?Q (4) ~T?Q (5) T (6) ~R（目标求反） 3.3 谓词逻辑的归结原理 问题：如何找归结对 例：P(x)?Q(y), ~P(f(y))?R(y) P(A)?Q(y), ~P(f(y))?R(y) 基本概念 置换 s={t1/v1, t2/v2, …, tn/vn} 对公式E实施置换s后得到的公式称为E的例，记作Es。 例：s1={z/x, Ay}, 则： P[x, f(y), B]s=P[z, f(A), B] 合一 如果存在一个S置换，使得{Ei}中 E1s=E2s