04-推理技术（经典推理）

推理技术（经典推理）

消解原理（谓词逻辑）

概念

文字：一个原子公式及其否定，$P(x)、 \lnot P(x)$

子句：文字的析取（或），$P(x) \lor Q(x)$

空子句：不包含任何子句的文字，用$NIL$

子句集：由子句或空子句构成的集合

消解：对谓词演算公式进行分解和化简，消去一些符号，得到子句

消解式：两个子句通过消解，得到的新子句

重言式：互补文字的文字，例如：$P(x)\lor \lnot P(x)$、$P(x)\lor Q(y) \lor \lnot P(x) \lor \lnot Q(y)$

求子句集的九个步骤

1. 消去蕴涵符号：$A \longrightarrow B <=> \lnot A \lor B$

2. 减少否定符号管辖范围；摩根定律和量词转换定律

   • $\lnot (A \lor B) <=> \lnot A \land \lnot B$
   • $\lnot (A \land B) <=> \lnot A \lor \lnot B$
   • $\lnot (\exists x)P(x) <=> \forall x[\lnot P(x)]$
   • $\lnot (\forall x)P(x) <=> \exists x[\lnot P(x)]$

3. 对变量标准化（改名）：不同量词辖域变量，使用不同变量名

4. 消去存在量词

   1. 是其他量词被包裹的：使用Skolem函数

      • 利用外层约束构造Skolem函数替换内层被约束变量

      • 例：$\forall y [(\exists x)P(x,y)] <=> \forall y P(g(y),y)$

   2. 没有被包裹：$(\exists x)P(x) <=> P(X)$ X是常量

5. 化为前束式：将全称量词都移到公式前面，量词部分称为前缀，后面称为母式

6. 将母式化为子句合取范式：使用分配律改为或的关系

   • 不使用$A \lor(B \land C) <=> (A \lor B) \land (A \lor C)$
   • ==$A \land (B \lor C) <=> (A \land B) \lor (A \land C)$==

7. 消去全称量词：$(\forall x)P(x) <=> P(y)$

8. 消去连接符号$\land$：使用$\{A,B\}$代替$A \land B$

9. 对集合中每个子句的变量进行唯一变量名更改(改名)

消解

不含变量的消解：两个子句，消去互补文字，剩下未消去的内容任然用子句连接符号$\lor$(或)进行连接

含变量的消解：两个子句，将可能互补的一对，置换为合一式，消去，其他非互补谓词中也要使用该置换进行置换，剩下未消去的内容任然用子句连接符号$\lor$(或)进行连接

消解反演证明问题

1. 定义谓词
2. 使用定义谓词将已知的知识（问题和要证明的结论）表示出来
3. 将问题和要证明的结论的否定分别求取子句集
4. 合并两个求取的子句集
5. 对新子句集使用消解原理，推出空子句即可证明

消解反演求解问题

1. 定义谓词
2. 使用定义谓词将已知的知识（问题和问题目标）表示出来
3. 将问题和问题目标的否定分别求取子句集
4. 对问题目标子句集中每个子句，构造重言式，加入到问题子句集中
5. 对新子句集使用消解原理，该子句集的根子句为求解问题的答案

规则演绎系统（产生式规则）

正向规则演绎系统

1. 将事实转换为与或形：只有文字的析取（或）和合取（与）

   1. 减少否定符号管辖范围；摩根定律和量词转换定律
   2. 对变量标准化（改名）：各项合取（与）变量名不同
   3. 消去存在量词，常量消去
   4. 化为前束式，后消除全称量词：将全称量词都移到公式前面，量词部分称为前缀，后面称为母式

2. 用与或图表示与或表达式：与关系层1连接符，或关系层k连接符

3. 与或图的F规则转换

   1. 将规则转换为单文字蕴含与或形公式：例：

      1. 左面是单文字，右面是与或形可转为与或图

      • $S \longrightarrow A \land B \lor C$
      • $A \lor B \longrightarrow C <=> A\longrightarrow C 、 B \longrightarrow C$
      • $A \land B \longrightarrow C 无效$

   2. 规则蕴含式左面单文字配匹的已知与或图节点，用匹配符连接规则蕴含式右的新与或图

4. 得到作为终止条件的目标公式

   1. 由与或树得到的子句集中出现就终止
   2. 子句集是析取层（或）父节点不同的节点组合

逆向规则演绎系统

1. 将事实转换为与或形：只有文字的析取（或）和合取（与）

   1. 减少否定符号管辖范围；摩根定律和量词转换定律
   2. 对变量标准化（改名）：与正向演绎相反，各项析取（或）变量名不同
   3. 消去存在量词，skolem函数消
   4. 化为前束式，后消除全称量词：将全称量词都移到公式前面，量词部分称为前缀，后面称为母式

2. 用与或图表示与或表达式：连接符与正向演绎相反，与关系层k连接符，或关系层1连接符

3. 与或图的B规则转换

   1. 将规则转换为与或形蕴含单文字公式：例：

      1. 右面是单文字，左面面是与或形可转为与或图

      • $A \land B \lor C\longrightarrow S$
      • $C \longrightarrow A \lor B <=> C\longrightarrow A 、 C \longrightarrow B$
      • $C \longrightarrow A \land B :无效$

   2. 规则蕴含式右面单文字配匹的已知与或图节点，用匹配符连接规则蕴含式右的新与或图

   3. 置换后与已知事实一致则证明成功

双向规则演绎系统

使用正向和反向演绎同时进行推理，正向和逆向叶节点都匹配了，则证明成功

产生式系统（产生式规则）

总数据库

• 存放初始证据
• 原始证据（证据不足询问的新证据）
• 中间结论
• 结果

规则库

• 规则集（一条条IF...THEN...）

控制策略

推理策略

• 推理方向
  • 正向推理：由总数据库的初始证据一步步得到结果
  • 反向推理：假设成立，一步步搜索支持假设的证据是否存在总数据库中
  • 双向推理：先正向或反向推理，推理不下去了，回头询问用户原始证据再接着推理
• 冲突消解：解决满足多条规则都满足的情况选则那条结论

搜索策略

搜索路线决定效率