消解原理（PPT）.ppt

* 例：某人被盗，派出所派出5个侦察员去调查。研究案情时，侦察员A说：“赵和钱至少有一个人作案”；侦察员B说：“钱和孙至少有一个人作案”；侦察员C说：“孙和李至少有一个人作案”；侦察员D说：“赵和孙至少有一个人与此案无关”；侦察员E说：“钱和李至少有一个人与此案无关”。如果这5个侦察员的话都可信的，试问谁是盗窃犯呢？ * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * 四、消解原理 概 述 归结原理 消解是一种可用于一定的子句公式的重要的推理规则 一个子句定义为由文字的析取组成的公式 一个原子公式和原子公式的否定叫做文字 子句与子句集 原子公式，简称原子：不含任何连接词的谓词公式。 文字：原子或原子的否定。 P(x), ? Q(x,y), R(x,y) 子句：由一些文字组成的析取式。 P(x,y)∨? Q(x,y)， P(x)∨R(x,y) 概 述 空子句：不含任何文字的子句，记为NIL。 空子句不含任何文字，它不能被任何解释满足，是永假的。 子句集：由子句构成的集合。 概 述 概 述 当消解可使用时，消解过程被应用于母体子句对，以便产生一个导出子句。 如果存在某个公理E1?E2和另一公理 ?E2?E3，那么E1?E3在逻辑上成立，这就是消解，而称E1?E3为E1?E2 和?E2?E3的消解式。 4.1 子句集的求取 步骤 （1）消去蕴涵符号 A?B ?A∨B （2）减少否定符号的辖域 ?(A∧B) ?A∨?B ?(A∨B) ?A∧?B ?(?A) A ?x(?A) ??x(A) ?x(?A) ??x(A) 子句集的求取 步骤 （3）对变量标准化 ?x{P(x)(?x)Q(x)} ?x{P(x)(?y)Q(y)} （4）消去存在量词 ?y[(?x)P(x,y)] ?y[P(g(y),y)] 规则：以一个Skolem函数代替每个出现的存在量词的量化变量。如果消去的存在量词不在任何一个全称量词的辖域内，那么就用不含变量的Skolem函数替换。 子句集的求取 步骤 （5）化为前束型 前束型=（前缀）（母式） （6）把母式化为合取范式 A∨(B∧C) {A∨B}∧{A∨C} 子句集的求取 全称量词串 无量词公式 步骤 （7）消去全称量词 （8）消去连词符号∧ （9）更换变量名称 子句集的求取 例： ?x{P(x)?{(?y)[P(y)?P(f(x,y))]∧?(?y)[Q(x,y)?P(y)]}} 子句集的求取 消去蕴涵符号 ?x{?P(x)∨{(?y)[P(y)?P(f(x,y))]∧?(?y)[Q(x,y)?P(y)]}} ?x{?P(x)∨{(?y)[?P(y)∨P(f(x,y))]∧?(?y)[?Q(x,y)∨P(y)]}} 减少否定符号 ?x{?P(x)∨{(?y)[?P(y)∨P(f(x,y))]∧(?y)[Q(x,y)∧?P(y)]}} 对变量标准化 ?x{?P(x)∨{(?y)[?P(y)∨P(f(x,y))]∧(?w)[Q(x,w)∧?P(w)]}} 子句集的求取 消去存在量词 ?x{?P(x)∨{(?y)[?P(y)∨P(f(x,y))]∧[Q(x,g(x))∧?P(g(x))]}} 化为前束形 (?x)(?y){?P(x)∨{[?P(y)∨P(f(x,y))]∧[Q(x,g(x))∧?P(g(x))]}} 母式化为合取范式 (?x)(?y){[?P(x)∨?P(y)∨P(f(x,y))]∧[?P(x)∨ Q(x,g(x))]∧[?P(x)∨?P(g(x))]} 子句集的求取 消去全称量词 {[?P(x)∨?P(y)∨P(f(x,y))]∧[?P(x)∨ Q(x,g(x))]∧[?P(x)∨?P(g(x))]} 消去∧ ?P(x)∨?P(y)∨P(f(x,y)) ?P(x)∨ Q(x,g(x)) ?P(x)∨?P(g(x)) 更换变量名 ?P(x1)∨?P(y)∨P(f(x1,y)) ?P(x2)∨ Q(x2,g(x)) ?P(x3)∨?P(g(x3)) 4.2 消解推理规则 消解推理规则