第Ⅲ部分 知识、推理与规划 第7章 逻辑Agent 中国科大 计算机学院.

Presentation on theme: "第Ⅲ部分 知识、推理与规划 第7章 逻辑Agent 中国科大 计算机学院."— Presentation transcript:

1 第Ⅲ部分 知识、推理与规划 第7章 逻辑Agent 中国科大 计算机学院

2 本章内容 7.1 基于知识的Agent 7.2 Wumαus世界 7.3 逻辑 7.4 命题逻辑：一种简单逻辑 7.5 命题逻辑定理证明
7.6 有效的命题逻辑模型检验 7.7 基于命题逻辑的Agent

3 命题逻辑定理证明 概述 推导和证明 归结证明 Hoγn子句和限定子句 前向和反向链接

4 概述 模型检验方法：枚举所有模型，并验证语句在所有模型中为真。
定理证明方法：在知识库的语句上直接应用推理规则已构建目标语句的证明，而无须关注模型。 如果模型数目庞大而证明很短，则定理证明就比模型检验更有效。 蕴含相关的几个概念： 逻辑等价 有效性 可满足性

5 逻辑等价 逻辑等价：两语句α 和是逻辑等价的，如果它们在同样的模型集合中为真，记为α≡。 逻辑等价的另一种定义：
对于任意两个语句α 和ß，α≡ß 当且仅当α|=β 且β|=α。

6 常用的逻辑等价 交换律： α∨β ≡ β ∨α ； α ∧ β ≡ β ∧ α 结合律： (α∨β) ∨ γ ≡ α∨(β ∨γ);
交换律： α∨β ≡ β ∨α ； 　 　 α ∧ β ≡ β ∧ α 结合律： (α∨β) ∨ γ ≡ α∨(β ∨γ);　 (α ∧ β) ∧ γ ≡ α ∧(β ∧ γ) 分配律： α∨(β∧γ) ≡ (α∨β)∧(α∨γ) ； α∧(β∨γ) ≡ (α∧β)∨(α∧γ) 双重否定律：α ≡ ¬¬α 等幂律：α ≡ α∨α； α ≡ α∧α 摩根律: ¬ (α∨β) ≡ ¬ α ∧ ¬ β ；　 　　 ¬ (α ∧β) ≡ ¬ α ∨ ¬ β 吸收律: α∨(α∧β ) ≡ α ；　 　　　　　α ∧(α∨β ) ≡ α 可用真值表证明

7 常用的逻辑等价 同一律: α∨0 ≡ α ； α∧1 ≡ α 零律：α∨1 ≡ 1； α∧0 ≡ 0 排中律：α∨¬α ≡ 1
同一律: α∨0 ≡ α ；　α∧1 ≡ α 零律：α∨1 ≡ 1；　α∧0 ≡ 0 排中律：α∨¬α ≡ 1 矛盾律：α∧¬α ≡ 0 蕴含等值式：α ⇒ β ≡ ¬ α∨β 等价等值式：α ⇔ β ≡ (α ⇒ β)∧(β ⇒ α) 假言易位式: α ⇒ β ≡ ¬ β ⇒ ¬ α 等价否定等值式：α ⇔ β ≡ ¬α ⇔ ¬β 归谬论：(α ⇒ β)∧(α ⇒ ¬β) ≡ ¬α 可用真值表证明

8 有效性 一个语句是有效的，如果在所有的模型中它都为真。 例如，语句PV¬P 为有效的。 有效语句也被称为重言式——它们必定为真。
也称作永真式。 因为语句True 在所有的模型中为真，每个有效语句都逻辑等价于True 。

9 可满足性 一个句子是可满足的，如果它在某些模型中为真。
例如，在先前给出的知识库中 (R1 ∧ R2 ∧ R3 ∧ R4 ∧ R5)是可满足的，因为存在3 个使得它为真的模型。 如果语句α 在模型m 中为真，那么称m 满足α ，或者称m 是α 的一个模型。 可以通过对可能的模型进行枚举直到发现某个满足该语句的模型来检验可满足性。命题逻辑语句的可满足性判定是第一个被证明为NP 完全问题的问题。

10 可满足性 计算机科学的很多问题实际上是可满足性问题。
例如，第6章中的所有约束满足问题本质上是询问问在某个赋值下约束是否为可满足的。通过适当变换，搜索问题也可以通过可满足性检验来求解。 有效性和可满足性必然是相关联的： α 是有效的，当且仅当¬ α 不可满足。 α 是可满足的，当且仅当¬ α不是有效的。

11 αI=ß当且仅当α ∧ ¬ß)是不可满足的。
可满足性 非常有用的结论： αI=ß当且仅当α ∧ ¬ß)是不可满足的。 通过验证(α∧¬β)的不可满足性，从α 证明ß ， 刚好符合归结的标准数学证明技术。 也称为反证法或矛盾法证明。 假定语句ß为假，并证明这将推导出和己知公理α 的一个矛盾。该矛盾正是说语句(α∧¬β)不可满足的含义。

12 命题逻辑定理证明 概述 推导和证明 归结证明 Hoγn子句和限定子句 前向和反向链接

13 常用的推理规则 分离规则(Modus Ponens)： 只要给定任何形式为α ⇒ β 的语句和α ，就可以推导出语句β 。 例如，如果己知
(WumpusAhead∧WumpusAlive) ⇒ Shoot 和(WumpusAhead∧WumpusAlive) ， 那么可以推导出Shoot。

14 常用的推理规则 与消去：可以从一个合取式推导出任何合取子句。
例如，从WumpusAhead∧WumpusAlive 可以推导出WumpusAlive 。 所有逻辑等价都可以作为推理规则。 例，用于双向蕴涵消去的等价给出两条推理规则：

15 Wumpus世界推理示例 Wumpus世界推理示例：从包含R1 到R5的知识库开始，说明如何证明¬P12，也就是说，证明[1, 2]中没有陷阱。 R1: ¬P11 R2: B11  (P12 V P21) R3: B21  (P11 V P22 V P31) R4: ¬B11 R5: B21 将双向蕴涵消去应用于R2，得到： R6：( B11⇒(P12 V P21) )∧( (P12 V P21)⇒B11 )

16 Wumpus世界推理示例 Wumpus世界推理示例： 对R6进行与消去，得到： R7: (P12 V P21)⇒B11
其逆否命题的逻辑等价给出： R8: ¬ B11 ⇒ ¬(P12 V P21) 对R8和感知信息R4(即¬B11)运用分离规则，得到 R9: ¬(P12 V P21) 应用摩根律，给出结论 R10: ¬P12∧¬P21 也就是说，P12和P21都不包含陷阱。

17 命题逻辑的推理 前述的推导过程 ——推理规则的应用序列——称为一个证明。
寻找证明的过程与搜索问题中寻找解的过程非常类似。实际上，如果定义后继函数以便生成推理规则所有可能的应用，那么第3章和第4章中的所有搜索算法可以用于寻找证明。因而，搜索证明是模型枚举的一个替换方法。 搜索过程可以从最初的知识库正向出发，应用推理规则以生成目标语句，或者从目标语句反向进行，试图找到由初始知识库引出的推理规则链。

18 命题逻辑的推理 命题逻辑的推理是NP 完全的。这个事实表明最坏的情况下，搜索证明的方法将不比模型的枚举方法更有效率。
然而，在很多实际情况中，寻找某个证明的过程可以更简单高效。因为无论寻找多少个命题，它都可以忽略不相关的命题。

19 命题逻辑的推理 例如，先前给出的可以推导出- ¬P12∧¬P21的证明没有提及命题B21、P11、P22 或P31 。
它们可以被忽略的原因在于，目标命题P12只在语句R4中出现，R4中的其它命题只在R4 和R2中出现。因此， R1、R3 和R5与证明过程无关。 即使我们把上百万的更多语句添加到知识库，最后结果还是相同的。 然而，简单的真值表算法将会由于模型的指数爆炸而失效。

20 命题逻辑的推理 逻辑系统的这一特征,本质上遵循一个更基本的、被称为单调性的概念。
单调性，意味着蕴涵语句集在信息被添加到知识阵的时候只会增长。对于任意语句α 和β ， 如果KBI= α ，那么KB∧β|=α 例，假设知识库包含附加断言ß，ß宣称世界中正好有8个陷阱。这条知识将有助于智能体提取出附加结论，但是它无法使得任意己经推导出的结论α无效——诸如[1, 2]中没有陷阱的结论。

21 命题逻辑的推理 单调性意味着任何时刻只要在知识库中发现了合理的前提，就可以应用推理规则——规则的结论一定遵循“与知识库中的其余内容无关”的要求。

22 命题逻辑定理证明 概述 推导和证明 归结证明 Hoγn子句和限定子句 前向和反向链接

23 归结 前面所涉及的推理规则都是可靠的，但是我们还没有对使用它们的推理算法的完备性问题进行讨论。
搜索算法，诸如选代深入搜索（第 节），在它们找到任何可到达的目标的意义上都是完备的。但是如果可用的推理规则是不充分的，那么目标将不可到达——即只应用那些推理规则找不到证明。 例如，如果我们除去双向蕴涵消去规则，前一节中的证明将无法继续。 归结：一个推理规则。当它和任何一个完备的搜索算法相结合时，可以得到一个完备的推理算法。

24 Wumpus世界的归结举例 智能体从[2, 1]返回[1, 1] ，接着走到[1, 2] ，它在此地感知到臭气，但没有微风。我们把下面的事实添加到知识库中： R11： ¬ B12 R12：B12  (P11VP22)VP13) 根据先前推导出R10 的同一过程，可以推导出[2, 2] 和[1, 3] 中没有陷阱（己知[1, 1]足没有陷阱的）： R13： ¬ P22 R14：¬ P13

25 Wumpus世界的归结举例 可以对R3应用双向蕴涵消去规则，接着对R5使用分离规则，得到[1, 1]、[2, 2]或[3, 1]中有陷阱的事实: R15：P11 V P22 V P31 现在第一次运用归结规则：R13 中的文字¬P22与R15中的文字P22 进行归结，得到 R16：P11VP31 用自然语言描述：如果[1, 1]、[2, 2]或[3, 1]中的某一个有陷阱，而且它不在[2, 2] 中，那么它在[1, 1]或[3, 1]中。

26 Wumpus世界的归结举例 类似地， R1中的文字¬P11与R16 中的文字P11进行归结，得到 R17：P31
用白然语言描述:如果[1, 1]或[3, 1]中有陷阱，而且它不在[1, 1] 中，那么它在[3, 1]中。 最后这两个推理步骤是单元归结推理规则的也例。

27 单元归结规则 上式为单元归结规则，其中，每个l都是一个文字，而且li和m是互补文字（即， 一个文字是另一个文字的否定式）。
因而，单元归结规则选取一个子句（文字的一个析取式）和一个文字，并生成一个新的子句。 注意单个文字可以被视为只有一个文字的析取式，也被称为单元子句。

28 全归结规则 上式为全归结规则，其中li和mj是互补文字。 如果只处理长度为2的子句，可以写为:
也就是说，归结选取两个子句并生成一个新的子句，该新子句包含除了两个互补文字以外的原始子句的所有文字。

29 归结规则 归结规则的一个技术：结果子句中每个文字只应包含一次。 去除文字的多余副本被称为归并。
例如，如果用(AV¬B)与(AVB)归结，则得到(AVA) ， 最终简化为A 。

30 归结规则 归结的可靠性： 如果li为真，那么mj假，因此m1∨...∨mj-1∨mj+I∨. ..∨mn必为真，因为己知m1∨...∨mn。
如果li为假，那么l1∨...∨li-1∨li+I∨. ..∨lk必为真，因为己知l1∨...∨lk 。 无论li为真还是为假，这些结论必定有一个成立——与归结规则的结果一致。

31 归结规则 归结规则形成了完备推理过程的基础。 对于命题逻辑的任意语句α和β，基于归结的定理证明器，能够确定α|=β是否成立。
但是：归结只在特定意义上是完备的。己知A为真，我们无法用归结来自动地生成结论A∨B。然而，我们可以用归结来回答A∨B 是否为真的问题。这称为反证法完备性，意思是归结总是可以用于确认或者反驳某个语句，但是它无法用于真值语句的枚举。

32 合取范式 归结规则只适用于文字的析取式，因此它看来只和知识库以及这样的析取式组成的查询有关。那么，对于所有的命题逻辑，它如何实现一个完备的推理过程? 答案：命题逻辑的每个语句逻辑上都等价于文字析取式的合取式。 以文字析取式的合取形式表达的语句被称为合取范式或者CNF（Conjunctive normal form）。

33 合取范式 以k-CNF 形式表示的语句每个子句正好有k 个文字： (l1,1∨...∨l1,k) ∧…∧ (ln,1∨...∨ln,k)

34 合取范式的转换过程举例 例，把B11  (P12∨P21)转换成合取范式。
消去双向蕴含 ，用(α ⇒ β) (β ⇒ α)代替(α  β)。 (B11⇒(P12∨P21)) ∧ ((P12∨P21)⇒B11) 消去蕴含⇒ ，用 ¬ α∨β代替α ⇒ β。 (¬B11∨P12∨P21) ∧ (¬(P12∨P21)∨B11)

35 合取范式的转换过程举例 例，把B11  (P12∨P21)转换成合取范式。 ……
CNF要求¬符号只出现在文字中，因此一般通过反复应用下列等值式“将¬否定词内移到文字中”。 双重否定律：α ≡ ¬¬α 摩根律: ¬ (α ∧β) ≡ ¬ α ∨ ¬ β　 　　 ¬ (α∨β) ≡ ¬ α ∧ ¬ β 对于本例，只需使用最后一条规则，得到： (¬B11∨P12∨P21) ∧ (¬P12∧¬P21)∨B11)

36 (¬B11∨P12∨P21)∧(¬P12∨B11)∧(¬P12∨¬P21))
合取范式的转换过程举例 例，把B11  (P12∨P21)转换成合取范式。 …… 至此，所得到的一个语句，包含了作用于文字的嵌套的∧和∨算符。运用分配律，在可能的位置上将∧对∨进行分配即可。 分配律：α∨(β∧γ) ≡ (α∨β)∧(α∨γ) ； 对于本例，得到一个CNF，3 个子句的合取式： (¬B11∨P12∨P21)∧(¬P12∨B11)∧(¬P12∨¬P21))

37 合取范式的转换过程 求合取范式的基本步骤： 削去对于{∨， ∧， ¬}来说冗余的联结词。 内移或削去否定号~。 利用分配率。
例：求取P ∧ (Q ⇒ R) ⇒ S 的合取范式 解： P ∧ (Q ⇒ R) ⇒ S 　　= ¬（P∧(¬ Q∨R) ∨S 　　= ¬ P∨ ¬(¬ Q∨R) ∨S 　　= ¬ P∨(¬ ¬ Q∧ ¬ R) ∨S 　　= ¬ P∨(Q∧ ¬ R) ∨S 　　= ¬ P∨S∨(Q∧ ¬ R) 　　= (¬ P∨S∨Q) ∧(¬ P∨S∨ ¬ R)

38 归结算法 基于归结的推理过程可以通过使用反证法证明原理而发挥作用。也就是说，为了证明KBI=α ，需要证明(KB∧¬α)是不可满足的。
归结算法的一般过程：首先，把(KB∧¬α)转换为CNF。接着，对结果子句运用归结规则。每对包含互补文字的子句相归结产生一个新的子句，如果该新子句尚未出现过，则将它加入子句集中。此过程将持续下去，直到发生以下两种情况之一： 没有可以添加的新语句，则α 不蕴涵β ； 使用归结规则可以生成空子句，则α 蕴涵ß。

39 归结算法 空子句表示矛盾： 空子句——没有析取子句的析取式——等价于False，因为只有当析取式至少有一个为真的析取子句，它才为真。
另一种了解空子句表示矛盾的方法是，观察到它只能是两个互补单元子句，如P 和¬P进行归结的结果。

40 归结算法 命题逻辑的一个简单归结算法。函数PL-RESOLVE 返回对它的两个输入进行归结得到的所有可能子句的集合。

41 Wumpus 世界中的归结推理 当智能体位于[1, 1]时，那里没有微风，因此在相邻的方格中不可能有陷阱。相关的知识库为：
KB = R2∧R4 = (B11(P12∨P21))∧¬ B11 而我们希望证明α ，也就是¬P12 。 证明过程：

42 例题 证明公式：(P ⇒ Q) ⇒ (¬ Q ⇒ ¬ P)
分别将公式前项化为合取范式：　P ⇒ Q ＝ ¬ P ∨ Q 　　结论求¬后的后项化为合取范式： 　　 ¬(¬ Q ⇒ ¬ P)＝ ¬(Q∨ ¬ P) ＝ ¬ Q ∧ P 　　两项合并后化为合取范式：（ ¬ P ∨ Q）∧ ¬ Q ∧ P 　　则子句集为： 　　{¬ P∨Q， ¬ Q，P} 　　对子句集中的子句进行归结可得： 　 1. ¬ P∨Q 　　2. ¬ Q 　　3. P 　　4. Q，（1，3归结） 　　5. □ ，（2，4归结） 　　由上可得原公式成立。

43 归结的完备性 子句集S 的归结闭包RC(S)：通过对S 中的子句或其派生子句反复应用归结规则而生成的所有于句的集合。
PL-RESOLUTION计算的归结闭包是变量clauses的终值。 RC(S)一定是有限的，因为用S 中出现的符号P1, ..., Pk只能构成有限多个不同的子句。注意，如果没有将重复的文字剔除的归并步骤，这可能不成立。因此， PL-RESOLUTION总是可终止的。

44 归结的完备性 命题逻辑中归结的完备性定理被称为基本归结定理：如果子句集是不可满足的，那么这些子句的归结闭包包含空子句。
通过证明这个定理的逆否命题，“如果闭包RC(S) 不包含空子句，那么S 是可满足的”，来证明这个定理。 实际上，可以用P1， …， PK的适当真值来构造S 的一个模型。构造过程如下：i 从1 到k ， 如果RC(S)中有一个包含文字¬ Pi的子句，该子句所有的其它文字在P1 ..., Pi-1的赋值下都为假，那么对Pi赋值false 。 否则，对Pi 赋值true。 还需要证明对P1， …， PK的赋值是S 的一个模型，倘若RC(S)在归结下是封闭的而且不包含空子句的话。

45 本章内容 7.1 基于知识的Agent 7.2 Wumαus世界 7.3 逻辑 7.4 命题逻辑：一种简单逻辑 7.5 命题逻辑定理证明
7.6 有效的命题逻辑模型检验 7.7 基于命题逻辑的Agent

46 有效的命题逻辑模型检验 一个完备的回溯算法 局部搜索算法 随机SAT问题现状

47 一个完备的回溯算法 DPLL算法：通常被称为戴维斯-普特南(Davis-Putnam) 算法，以Martin Davis 和Hilary Putnam (1960)的开创性论文命名。实际上，该算法是Davis 、Logemann 和Loveland (1962) 描述的版本，因此习惯按最初的这4 个作者首字母缩写将其命名为DPLL。 DPLL 质上是一个对可能模型的递归深度优先枚举算法。

48 一个完备的回溯算法 DPLL算法

49 局部搜索算法 到目前为止，教材中的多种局部搜索算法，包括HlLL-CLIMBING和SIMULATED-ANNEALING，可以直接应用于可满足性问题，倘若我们能选择出正确的评价函数。 因为目标是寻找满足每个子句的一个赋值，统计未满足子句的数量的评价函数将负责这项工作。 实际上，这正是CSP中MIN-CONFLICT算法采用的度量方法。 所有这些算法涉足完全赋值空间，每次翻转一个符号的真值。该赋值空间通常包括很多局部极小点，为了避开局部极小值，需要采用不同形式的随机方法。近年来，人们做了大量实验以便找到贪婪性和随机性之间的良好平衡点。

50 局部搜索算法 WALKSAT 是从所有的这类工作中涌现出来的最简洁有效的算法之一。
(1)"最小冲突"步骤，最小化新状态下未满足语句的数量，以及 (2) “随机行走”步骤，随机挑选符号。

51 局部搜索算法 WALKSAT算法

52 随机SAT问题现状 有些SAT问题十分困难。 容易的问题可以用任何旧算法来解决。
但SAT问题是NP完全的，至少有一些问题实例需要指数级的运行时间。 对于特定种类问题，有一些令人惊讶的发现。 例如， n皇后问题——被认为对于回溯搜索算法是相当棘手的——对于局部搜索方法，比如最小冲突法，却非常的容易。这是因为解非常稠密地分布在赋值空间上，任意初始赋值都可以保证在其附近存在某个解。故此n 皇后问题易于求解，因为它是约束过少的。

53 随机SAT问题现状 在考虑合取范式形式的可满足性问题的时候，约束过少的问题是一个具有相对较少的子句来约束变量的问题。
对于随机语句源，最困难的问题的“子句数/符号数”的比值大概是4.3.

54 本章内容 7.1 基于知识的Agent 7.2 Wumαus世界 7.3 逻辑 7.4 命题逻辑：一种简单逻辑 7.5 命题逻辑定理证明
7.6 有效的命题逻辑模型检验 7.7 基于命题逻辑的Agent

55 基于命题逻辑的Agent 核心：构造基于命题逻辑的Wumpus世界智能体。 世界的当前状态 Wumpus世界中当前状态的推理问题
命题知识库表示世界，问题请求解搜索和领域专用代码确定采取哪个行的 逻辑状态评估 利用已有的推理结果。 通过命题推理制定计划 用逻辑推理来知道计划。 课后阅读

56 本章小结 逻辑的基本概念 命题逻辑（语法、语义、模型检验、定理证明） 有效的命题逻辑模型检验方法 DPLL和WalkSAT

57 课堂练习 试使用归结法证明下列命题的正确性。 α ⇒(β ⇒ α) (α ⇒(β ⇒ γ)) ⇒ ((α ⇒ β) ⇒(α ⇒ γ))
(β ⇒ ¬α) ⇒((β ⇒ α) ⇒ ¬β)

58 [(Food⇒Party)∨(Drinks⇒Party)]⇒[(Food∧Drinks)⇒Party)]
作业 （习题7.18）考察下述语句： [(Food⇒Party)∨(Drinks⇒Party)]⇒[(Food∧Drinks)⇒Party)] 通过枚举判定这个语句是有效的、可满足的（不是有效的），或不可满足的。 将蕴含句的左边和右边都转换为CNF，写出步骤，并解释转换的结果如何证实你在（a）中的答案。 利用归结证明（a）。