4.4-归结演绎推理-1.pdf

第4章确定性推理  4.1 推理的基本概念  4.2 推理的逻辑基础  4.3 自然演绎推理  4.4 归结演绎推理(1) 4.4 归结演绎推理  归结演绎推理是一种基于鲁宾逊（Robinson ）归结原理的机器推理技 术。鲁宾逊归结原理亦称为消解原理，是鲁宾逊于1965年在海伯伦 （Herbrand ）理论的基础上提出的一种基于逻辑的“反证法”。  在人工智能中，几乎所有的问题都可以转化为一个定理证明问题。定 理证明的实质，就是要对前提P和结论Q，证明P→Q永真。  由4.2节可知，要证明P→Q永真，就是要证明P→Q在任何一个非空的 个体域上都是永真的。这将是非常困难的，甚至是不可实现的。  为此，人们进行了大量的探索，后来发现可以采用反证法的思想，把 关于永真性的证明转化为关于不可满足性的证明。  即要证明P→Q永真，只要能够证明P ∧﹁Q是不可满足的就可以了(原 因是﹁(P→Q) ⇔ ﹁( ﹁P ∨Q) ⇔P ∧﹁Q 。  这方面最有成效的工作就是鲁宾逊归结原理。它使定理证明的机械化 成为现实。 4.4 归结演绎推理  4.4.1 子句集及其化简  4.4.2 鲁滨逊归结原理  4.4.3 归结反演推理的归结策略  4.4.4 用归结反演求取问题的答案 4.4.1 子句型 1. 子句与子句集  定义4.11 原子谓词公式及其否定统称为文字。  例如，P(x)、Q(x)、﹁P(x)、﹁Q(x)等都是文字。  定义4.12 任何文字的析取式称为子句。  例如，P(x) ∨Q(x)，P(x，f(x))∨Q(x，g(x))都是子句。  定义4.13 不含任何文字的子句称为空子句。  由于空子句不含有任何文字，也就不能被任何解释所满足， 因此空子句是永假的，不可满足的。  空子句一般被记为□或NIL 。  定义4.14 由子句或空子句所构成的集合称为子句集。 4.4.1 子句型 2. 子句集的化简(1/6)  在谓词逻辑中，任何一个谓词公式都可以通过应用等价关系及推理 规则化成相应的子句集。其化简步骤如下：  (1) 消去连接词“→”和“↔”  反复使用如下等价公式：  P→Q ⇔﹁P ∨Q  P↔Q ⇔ (P ∧Q)∨( ﹁P ∧﹁Q)  即可消去谓词公式中的连接词“→”和“↔”。  例如公式  (∀x)((∀y)P(x,y)→ ﹁(∀y)(Q(x,y)→R(x,y)))  经等价变化后为  (∀x)( ﹁(∀y)P(x,y) ∨﹁(∀y)( ﹁Q(x,y)∨R(x,y))) 4.4.1 子句型 2. 子句集的化简(2/6)  (2) 减少否定符号的辖域  反复使用双重否定率  ﹁( ﹁P) ⇔P  摩根定律  ﹁(P∧Q) ⇔﹁P ∨﹁Q  ﹁(P∨Q) ⇔﹁P ∧﹁Q  量词转换率  ﹁(∀x)P(x) ⇔ (∃x) ﹁P(x)  ﹁(∃x)P(x) ⇔ (∀x)￢P(x)  将每个否定符号“﹁”移到仅靠谓词的位置，使得每个否定符号最 多只作用于一个谓词上。  例如，上式经等价变换后为  (∀x)((∃y) ﹁P(x，y) ∨(∃y)( Q(x ，y) ∧﹁R(x，y))) 4.4.1 子句型 2. 子句集的化简(3/6)  (3) 对变元标准化  在一个量词的辖域内，把谓词公式中受该量词约束的变元全部用 另外一个没有出现过的任意变元代替，使不同量词约束的变元有不 同的名字。  例如，上式经变换后为  (∀x)((∃y)