人工智能原理 第3章 逻辑系统.

Presentation on theme: "人工智能原理 第3章 逻辑系统."— Presentation transcript:

1 人工智能原理 第3章 逻辑系统

2 第3章 逻辑系统 本章内容 命题逻辑和一阶谓词逻辑 3.2 逻辑系统的语法和语义 3.3 逻辑推理举例 3.4 逻辑智能体的推理策略 参考书目 附录 形式系统简介

3 经典数理逻辑 AI研究内容之一是推理，即研究怎样使计算机获得自动推理的能力
第3章 逻辑系统 经典数理逻辑 AI研究内容之一是推理，即研究怎样使计算机获得自动推理的能力 数理逻辑用数学方法研究各种推理中的逻辑问题，以推理本身作为研究对象 AI要使用逻辑推理，就必然涉及数理逻辑 / 数理逻辑的经典部分—经典的命题逻辑和一阶谓词逻辑，同时作为人工智能的知识表示方法和推理方法而存在；因此数理逻辑是人工智能的一个基础

4 逻辑智能体 基于知识的智能体的核心部件是知识库，当这些知识以逻辑形式表示并进行相应的推理时，就是逻辑智能体
第3章 逻辑系统 逻辑智能体 基于知识的智能体的核心部件是知识库，当这些知识以逻辑形式表示并进行相应的推理时，就是逻辑智能体 知识表示：命题逻辑、一阶谓词逻辑 推理(一阶谓词逻辑)—主要有3类推理算法：前向链接和演绎系统、反向链接和逻辑程序设计(本章)、归结反演和定理证明系统(第4章) 采用命题和谓词演算进行推理的系统(如演绎系统)是一种典型的逻辑智能体

5 3.1 命题逻辑和一阶谓词逻辑 命题、真值、原子公式、合式公式 谓词、论域、个体 量词、变量、函数 一阶语言、一阶语言的项
第3章 逻辑系统 3.1 命题逻辑和一阶谓词逻辑 命题、真值、原子公式、合式公式 谓词、论域、个体 量词、变量、函数 一阶语言、一阶语言的项

6 命题 命题：描述客观世界的可区分真假的陈述句, 即判断（经典二值逻辑：非真即假） 是命题的例子：
第3章 逻辑系统 命题 命题：描述客观世界的可区分真假的陈述句, 即判断（经典二值逻辑：非真即假） 是命题的例子： 2+2=4 / 二月份有30天 / 2002年哈尔滨有地震 / 人类能够证明数论中所有论断非真即假（有待时间） 不是命题的例子： 张三比李四聪明 / 公共汽车内非常拥挤（各人认识不同）

7 命题变量与真值 命题变量（变元）：一个命题用符号表示，称为命题符号 当命题符号代表任一个命题时，即为命题变量
第3章 逻辑系统 命题变量与真值 命题变量（变元）：一个命题用符号表示，称为命题符号 当命题符号代表任一个命题时，即为命题变量 真值：真或假 – 一个命题或命题变量具有真值 真值连接词（5个）：否定/合取/析取/蕴涵/等价

8 第3章 逻辑系统 简单命题与复合命题 真值函数：真值联结词可以视为一元或二元映射(真值函数)，￢是从{T,F}到{T,F}，其余是{T,F}2到{T,F}的映射 / 其函数定义由真值表确定 简单命题：一个被视为整体的、具有真或假的命题是简单命题； 复合命题：使用联结词将简单命题联结起来的命题是复合命题

9 命题语言与原子公式 命题逻辑：研究复合命题之间的推导关系
第3章 逻辑系统 命题语言与原子公式 命题逻辑：研究复合命题之间的推导关系 命题语言：是命题逻辑使用的形式语言，是符号的集合,用Lp表示 / 包括：命题符号、连接词、左右括号 原子公式：命题语言中的一个表达式是原子公式，当且仅当它是一个命题符号 / 原子公式也称为文字(包括正文字和负文字)

10 第3章 逻辑系统 命题逻辑的合式公式 合式公式(well-formed formula)，简称公式，记作wff：一个表达式是一个公式，当且仅当它能通过有限次地使用下述步骤生成： (1)原子公式是公式； (2)如果A是公式，则(￢A)是公式； (3)如果A、B均为公式，则A*B是公式，其中*表示∧∨→≡中的任意一个 / 公式的形成规则 / 命题逻辑的主要研究对象是公式

11 谓词 从命题到一阶谓词：命题内部逻辑结构的分解  对判断的分解，把判断中的具体内容抽出，称为个体；剩下的判断即为谓词
第3章 逻辑系统 谓词 从命题到一阶谓词：命题内部逻辑结构的分解  对判断的分解，把判断中的具体内容抽出，称为个体；剩下的判断即为谓词 谓词可看作是从个体域或个体域的笛卡儿乘积到真值集合{T/F}的映射 典型的推理例子：(1)凡人皆有死；(2)苏格拉底是人；(3)苏格拉底有死。（三段论式）M(x)D(x), M(s)├ D(s)

12 论域与个体 论域和个体：在一阶逻辑中，被研究对象构成的非空集称为论域；论域中的每个元素称为个体
第3章 逻辑系统 论域与个体 论域和个体：在一阶逻辑中，被研究对象构成的非空集称为论域；论域中的每个元素称为个体 论域例子：前面例子中的论域是“人” / 所有的有理数都是实数：其论域为有理数 一阶逻辑还研究个体之间的关系（或个体的性质）及作用于个体的函数 论域/个体/个体间关系/作用于个体函数 这4个成分构成了一阶逻辑的结构

13 谓词 谓词（关系）：一阶形式语言中用于指称论域中个体的性质或者个体之间关系的形式符号（大写字母表示） 给定了论域，就确定了谓词的真假值
第3章 逻辑系统 谓词 谓词（关系）：一阶形式语言中用于指称论域中个体的性质或者个体之间关系的形式符号（大写字母表示） 给定了论域，就确定了谓词的真假值 一元谓词：个体的性质；二元谓词(多元谓词)：个体的关系 个体的位置—空位，具体化—构成意义完整的语句 空位的数目—谓词的元数→几元谓词

14 量词与变量 变量(变元)：表示论域内的任意一个个体 / 常量(常元)，表示确定的个体 量词与变量：量词用来表示谓词的判断特性
第3章 逻辑系统 量词与变量 变量(变元)：表示论域内的任意一个个体 / 常量(常元)，表示确定的个体 量词与变量：量词用来表示谓词的判断特性 全称量词：对所有的x x P(x) 存在量词：存在x x P(x) 约束变量：、中x的变量，量词所管辖的公式如P(x)称为量词辖域 自由变量：不在量词辖域内的变量为自由变量

15 约束变量和自由变量 区别：自由变量可代入常量，约束变量不行，因为a P(a)无意义 ；约束变量可改名，自由变量不行
第3章 逻辑系统 约束变量和自由变量 区别：自由变量可代入常量，约束变量不行，因为a P(a)无意义 ；约束变量可改名，自由变量不行 带有全称变量x的命题表示为一阶公式时，其表示形式为 x(P(x)→…)，带有存在变量x的命题则表示形式为x(P(x)∧…) 例子：所有有理数都是实数 x(P(x)→R(x))，有些人身高超过2米x(M(x)∧G(x)) 上述使用方式不可改变，否则造成逻辑错误

16 函数 函数：表示个体之间的运算，可作用于一个或数个个体（用小写字母） 给定一个或若干个体（对象），产生一个新的个体（对象）/ 函数的元数
第3章 逻辑系统 函数 函数：表示个体之间的运算，可作用于一个或数个个体（用小写字母） 给定一个或若干个体（对象），产生一个新的个体（对象）/ 函数的元数 例子：x的父亲 father(张三) 两数之和仍是一个数 add(e1, e2)

17 函数与谓词的区别 谓词和函数的区别：谓词代表语句，结果是关系（具有真假值）；函数代表关系运算，结果是一个新个体
第3章 逻辑系统 函数与谓词的区别 谓词和函数的区别：谓词代表语句，结果是关系（具有真假值）；函数代表关系运算，结果是一个新个体 例子：谓词SUM(e1, e2, e3) 说明e1、e2、e3之间的关系是e1与e2的和是e3 ， 函数add(e1, e2)说明e1与e2相加的结果仍是一个数

18 一阶语言(1) 一阶语言L：是一阶逻辑使用的形式语言，可以和任何结构（论域）没有联系，也可以与某个结构有联系
第3章 逻辑系统 一阶语言(1) 一阶语言L：是一阶逻辑使用的形式语言，可以和任何结构（论域）没有联系，也可以与某个结构有联系 与结构没有联系的一阶语言由8类符号组成： (1)无限序列的个体符号（个体常量） (2)无限序列的谓词符号，有确定的元数n≥1 有一个特殊的谓词符号称为相等符号（等式），记为=。 L可含或不含=，如果含有，即称为含=的一阶逻辑

19 一阶语言(2) (3)无限序列的函数符号，有确定的元数m≥1 (4)无限序列的自由变量：用u/v/w等表示自由变量
第3章 逻辑系统 一阶语言(2) (3)无限序列的函数符号，有确定的元数m≥1 (4)无限序列的自由变量：用u/v/w等表示自由变量 (5)无限序列的约束变量：用x/y/z等表示约束变量 (6)联结词：￢∧∨→≡ (7)量词： 、 (8)标点：左右括号、逗号 ( ) ,

20 一阶语言的项和公式 L的项：一阶语言中的一个符号是项t，当且仅当它能通过有限次使用下述步骤生成：
第3章 逻辑系统 一阶语言的项和公式 L的项：一阶语言中的一个符号是项t，当且仅当它能通过有限次使用下述步骤生成： (1)个体常量、自由变量是项； (2)如果t1…tn是项，且f是n元函数，则f(t1…tn)是项 L的原子公式：一阶语言中的一个表达式是一个原子公式，当且仅当它有如下2种形式： (1)F(t1…tn)，F是n元谓词，t1…tn是项； (2)=(t1,t2)或t1=t2， t1、t2是项

21 一阶语言的公式(1) L的公式：一阶语言中的一个表达式是一个公式，当且仅当它能通过有限次使用下述步骤生成： (1)原子公式是公式；
第3章 逻辑系统 一阶语言的公式(1) L的公式：一阶语言中的一个表达式是一个公式，当且仅当它能通过有限次使用下述步骤生成： (1)原子公式是公式； (2)如果A是公式，则(￢A)是公式； (3)如果A、B均为公式，则A*B是公式，其中*表示∧∨→≡中的任意一个 (4)如果A(u)是公式，且x不在A(u)中出现，则x A(x)、x A(x)都是公式

22 一阶语言的公式(2) 一阶谓词公式的例子 数学命题的表示：5只被1和5整除
第3章 逻辑系统 一阶语言的公式(2) 一阶谓词公式的例子 数学命题的表示：5只被1和5整除 设Q(x,y)表示x被y整除，N(x)表示x是自然数  x(Q(5,x)→N(5)∨N(1)) 自然语言语句的表示：他不能在所有时刻欺骗所有人 设F(x)表示“x是人”/G(x)“x是一个时刻”/H(x,y)“他能在y时刻欺骗x”  ¬ x y (F(x)∧G(y) → H(x,y)) 或者 xy(¬H(x,y)∧F(x)∧G(y))

23 3.2 逻辑系统的语法和语义 逻辑系统的语法 逻辑系统的语义 语法和语义之间的关系
第3章 逻辑系统 3.2 逻辑系统的语法和语义 逻辑系统的语法 逻辑系统的语义 语法和语义之间的关系

24 逻辑系统 逻辑系统(亦称形式系统Formal System)由5个部分组成：
第3章 逻辑系统 逻辑系统 逻辑系统(亦称形式系统Formal System)由5个部分组成： 符号表—非空集合，即逻辑(形式)语言—如一阶语言 上全体符号的集合*的子集—项和变量 *的子集—公式 | 公式和项的交集为空 公式FORMULA上的子集—公理AXIOM 公式上的n元关系集合—推理规则RULE 、项TERM、FORMULA称为FS的组成部分 / AXIOM、RULE称为FS的推演部分

25 语法和形式推演 逻辑系统除符号表以外的部分构成了逻辑系统的语法
第3章 逻辑系统 语法和形式推演 逻辑系统除符号表以外的部分构成了逻辑系统的语法 形式推演：定义了公式之间的形式可推演性关系，它涉及公式的语法结构，其正确性能够机械地证明 用记号├ 表示形式可推演关系，读作“推出” 用├ A表示A是由形式可推演的（或形式可证明的），其中是前提，A是结论

26 推演规则举例 形式推演由形式推演规则定义，举例如下： 公式变换 A→B  AB 自反 A├ A (Ref)
第3章 逻辑系统 推演规则举例 形式推演由形式推演规则定义，举例如下： 自反 A├ A (Ref) 传递 if ├  ‘├ A then ├ A () ￢消去(反证律) if  , ￢A├ B &  , ￢A├￢B then ├ A (￢–) 公式变换 A→B  AB

27 第3章 逻辑系统 形式可推演性 形式可推演性：在命题/一阶逻辑系统中，A是由可形式推演的(或形式可证明的)，记为├A，当且仅当├A能通过有限次应用相应逻辑的形式推演规则生成 即├A成立，当且仅当存在有限序列使得 1├A1，2├A2，…，n├An 中的每一项均由某个形式推导规则生成,且n├An 就是├A即n=,An=A 建立在上述形式推演规则基础上的形式推演系统称为自然推演(演绎)系统

28 逻辑系统的语义 语义即对形式语言进行解释 赋予形式系统的论域及解释称为形式系统的语义结构，简称结构(structure) 第3章 逻辑系统
研究可推导性即形式推演(├)时不考虑作为前提和结论的命题的内容，只考虑命题真假并由此确定前提的真是否蕴涵结论的真，即前提和结论之间是否有可推导关系(语法) 研究形式系统的语义时，对逻辑系统赋予研究对象的集合即论域；用论域中的个体对象、对象之上的运算(函数)、对象之间的关系(谓词)去解释逻辑系统中的符号，称作指称denote  指称语义学 赋予形式系统的论域及解释称为形式系统的语义结构，简称结构(structure)

29 命题逻辑的语义与可满足性 研究命题逻辑的语义，即研究公式(公式集)的真假赋值问题
第3章 逻辑系统 命题逻辑的语义与可满足性 研究命题逻辑的语义，即研究公式(公式集)的真假赋值问题 真假赋值：真假赋值是以所有命题符号的集合为定义域、以真假值{1,0}为值域的函数。真假赋值v给公式A指派的值记作Av 可满足性：是可满足的，当且仅当有真假赋值v，使得v=1。此时称v满足。

30 第3章 逻辑系统 可满足性 的可满足性蕴涵了中所有公式的可满足性，但反过来不成立。因为这要求同一个真假赋值满足所有的公式(并非所有可满足的公式使用同一个赋值) 重言式和矛盾式 A是重言式(永真式)，当且仅当对于任意的真假赋值v，Av=1 A是矛盾式(永假式)，当且仅当对于任意的真假赋值v，Av=0

31 真假判断与逻辑推论 一个命题公式是重言式或者是矛盾式或者两者都不是，需要进行判定。判定方法可通过构造真假值表方法或采用树形分支的方法来判定
第3章 逻辑系统 真假判断与逻辑推论 一个命题公式是重言式或者是矛盾式或者两者都不是，需要进行判定。判定方法可通过构造真假值表方法或采用树形分支的方法来判定 可推导关系：研究前提的真是否蕴涵结论的真，引入语义以后对公式进行真假赋值；如果对任意的真假赋值，都有上述关系，则说明前提和结论之间存在一种逻辑推论关系(或称逻辑蕴涵)

32 第3章 逻辑系统 命题逻辑的逻辑推论 逻辑推论：设、A分别是命题逻辑中的公式集合和公式,A是的逻辑推论，记为 A，当且仅当对于任意真假赋值v，v=1蕴涵Av=1。 |=可读作“逻辑地蕴涵”，|=是前提和结论A之间的关系 逻辑推论的证明 要证明|=A时，即要证明对于任何真假赋值v，如果v=1则Av=1 (通常使用反证法)

33 一阶语言的语义 一阶语言的语义：一阶语言的解释包括一个论域和一个函数 函数把一阶语言中的个体符号映射到论域中的个体
第3章 逻辑系统 一阶语言的语义 一阶语言的语义：一阶语言的解释包括一个论域和一个函数 函数把一阶语言中的个体符号映射到论域中的个体 n元关系符号(即谓词)映射到论域上的n元关系 m元函数符号映射到论域上的m元全函数 以上组成了该论域中对一阶语言的解释

34 一阶语言的赋值 赋值：一阶语言L的赋值v包括一个论域D和一个函数(记作v) L中所有个体符号a为定义域，其赋值v(a)或av
第3章 逻辑系统 一阶语言的赋值 赋值：一阶语言L的赋值v包括一个论域D和一个函数(记作v) L中所有个体符号a为定义域，其赋值v(a)或av 关系符号F的赋值v(F)或Fv 函数符号f的赋值v(f)或fv 自由变量符号u的赋值v(u)或uv 则有 (1)av, uv∈D (2)FvDn (3)fv: Dm→D

35 一阶逻辑的逻辑推论 公式的真假值：一阶语言的公式在以D为论域的赋值之下，其真假值可以递归定义
第3章 逻辑系统 一阶逻辑的逻辑推论 公式的真假值：一阶语言的公式在以D为论域的赋值之下，其真假值可以递归定义 一阶逻辑的逻辑推论: 与命题逻辑相同，只是这里不使用真假赋值，而用赋值 逻辑推论：设、A分别是一阶语言的公式集和公式，A是的逻辑推论，记作|=A，当且仅当对于任何赋值v，v=1蕴涵Av=1 一阶逻辑的逻辑推论证明方法类似于命题逻辑，常用反证法。但对于否证逻辑推论，则需要构造赋值所需的论域。确定论域时，关键在于论域的大小

36 逻辑系统的整体特征 在经典逻辑的形式系统中，形式推演是语法概念，逻辑推论是语义概念
第3章 逻辑系统 逻辑系统的整体特征 在经典逻辑的形式系统中，形式推演是语法概念，逻辑推论是语义概念 形式系统的整体特征：是在形式系统引入语义以后，研究对于任何一阶语言的公式集和公式A在何种赋值的条件下，其结果是否为真—即研究形式推演与逻辑推论之间的关系 赋值的条件： 给定某个赋值—可满足性 给定任意赋值—有效性

37 可靠性定理与完备性定理 对于任何一阶语言的公式集和公式A，
第3章 逻辑系统 可靠性定理与完备性定理 对于任何一阶语言的公式集和公式A， ├ A|=A表示：凡是形式可推演性所反映的前提和结论之间的关系，在非形式的推理中都是成立的，即形式可推演性对于反映非形式的推理是可靠的，此即可靠性定理(或者称合理性) |=A ├ A表示：凡是在非形式推理中成立的前提和结论之间的关系，形式可推演性都是能够反映的，即形式可推演性在反映非形式推理时没有遗漏，此即完备性定理

38 可满足性与有效性(1) 不加证明地给出有关定义和定理
第3章 逻辑系统 可满足性与有效性(1) 不加证明地给出有关定义和定理 可满足性—一阶逻辑公式集合是可满足的，当且仅当有(以某个不空集为论域)赋值v，使得v=1 / 当v=1时，称v满足 反过来，不可满足性就是对任意论域上的任意赋值都有v=0

39 可满足性与有效性(2) 有效性：一阶逻辑公式A是有效的，当且仅当对于(以任何不空集为论域)任何赋值v，Av=1 / 有效性也称为普遍有效性
第3章 逻辑系统 可满足性与有效性(2) 有效性：一阶逻辑公式A是有效的，当且仅当对于(以任何不空集为论域)任何赋值v，Av=1 / 有效性也称为普遍有效性 论域中的可满足性、有效性： (1)在D中是可满足的，当且仅当有以D为论域的赋值v，使得v=1 (2)A在D中是有效的，当且仅当对于任何以D为论域的赋值v，Av=1

40 可满足性与有效性(3) (关于命题的)定理: (1)A是可满足的，当且仅当¬A是不有效的；(2)A是有效的，当且仅当¬A是不可满足的。
第3章 逻辑系统 可满足性与有效性(3) (关于命题的)定理: (1)A是可满足的，当且仅当¬A是不有效的；(2)A是有效的，当且仅当¬A是不可满足的。 (关于一阶的)定理: (1)A(u1,…,un)是可满足的，当且仅当x1... xn A(x1,…,xn)是可满足的 (2)A(u1,…,un)是有效的，当且仅当x1... xn A(x1,…,xn)是有效的

41 可靠性定理 可靠性定理[1]：设Form(L)，A∈Form(L)(也包括了命题语言Lp) (1)如果├A，则|=A；
第3章 逻辑系统 可靠性定理 可靠性定理[1]：设Form(L)，A∈Form(L)(也包括了命题语言Lp) (1)如果├A，则|=A； (2)如果├A，则|=A(即所有形式可推演的都是有效的) 协调性(无矛盾性)： Form(L)是协调的，当且仅当不存在A ∈Form(L)，使得├A且├ ¬A 可靠性定理[2]：设Form(L)，A∈Form(L) (1)如果是可满足的，则是协调的； (2)如果A是可满足的，则A是协调的。([1][2]等价)

42 完备性定理 命题逻辑和一阶逻辑的完备性 定理[1]:设 Form(L)，A∈Form(L)(含Lp)
第3章 逻辑系统 完备性定理 命题逻辑和一阶逻辑的完备性 定理[1]:设 Form(L)，A∈Form(L)(含Lp) (1)如果是协调的，则是可满足的； (2)如果A是协调的，则A是可满足的。 定理[2]:设 Form(L)，A∈Form(L) (1)如果|=A，则├ A； (2)如果|=A，则├ A(所有有效公式都是形式可证明公式)。 如果对论域限定以后，可得更精确的陈述

43 3.3 逻辑推理举例 wumpus世界 命题逻辑推理模式 基于电路的智能体
第3章 逻辑系统 3.3 逻辑推理举例 wumpus世界 命题逻辑推理模式 基于电路的智能体

44 wumpus世界(1) Wumpus是一个早期电脑游戏中的怪物 Agent感知： 陷阱和怪物的位置随机生成 第3章 逻辑系统 Gold
陷阱旁边有微风breeze 怪兽旁边有恶臭stench 金子闪闪发光glitter 感觉墙的反弹 陷阱和怪物的位置随机生成 stench Breeze Pit Wumpus (Monster) Stench Gold Agent

45 wumpus世界(2) Wumpus世界搜索图示—感知用5元组表示 第3章 逻辑系统 
A=Agent B=Breeze G=Glitter,Gold OK=safe square P=Pit S=Stench V=visited W=wumpus N=None 1,4 2,4 3,4 4,4 1,3 2,3 3,3 4,3 1,2 OK 2,2 3,2 4,2 1,1 A 2,1 3,1 4,1 1,4 2,4 3,4 4,4 1,3 2,3 3,3 4,3 1,2 OK 2,2 P? 3,2 4,2 1,1 V 2,1 A B 3,1 4,1  (a) [N,N,N,N,N] (b) [N,B,N,N,N]

46 第3章 逻辑系统 wumpus世界(3) A=Agent B=Breeze G=Glitter,Gold OK=safe square P=Pit S=Stench V=visited W=wumpus N=None 1,4 2,4 3,4 4,4 1,3 W! 2,3 3,3 4,3 1,2 A S OK 2,2 3,2 4,2 1,1 V 2,1 B 3,1 P! 4,1 1,4 2,4 P？ 3,4 4,4 1,3 W! 2,3 A B S G 3,3 4,3 1,2 S V OK 2,2 3,2 4,2 1,1 2,1 B 3,1 P! 4,1   (c) [S,N,N,N,N] (d) [S,B,G,N,N]

47 wumpus世界中的命题和推理规则 只考虑陷阱的情况 Pi,j=T— [i,j]中有陷阱，记为Pi,j
第3章 逻辑系统 wumpus世界中的命题和推理规则 只考虑陷阱的情况 Pi,j=T— [i,j]中有陷阱，记为Pi,j Bi,j=T — [i,j]中有微风，记为Bi,j 规则如下： R1 P1,1 R2 B1,1P1,2P2,1 R3 B2,1P1,1P2,2P3,1 R4 B1,1 R5 B2,1

48 第3章 逻辑系统 命题逻辑推理模式 分离规则 与消去 逻辑等价(双向蕴涵消去)

49 wumpus世界的推理例子 用R1~R5规则和推理模式证明：[1,2]和[2,1]中没有陷阱，即P1,2和P2,1 证明： 从R2开始
第3章 逻辑系统 wumpus世界的推理例子 用R1~R5规则和推理模式证明：[1,2]和[2,1]中没有陷阱，即P1,2和P2,1 证明： 从R2开始 R6 (B1,1(P1,2∨P2,1))∧((P1,2∨P2,1)B1,1) R2双向蕴涵消去 R7 (P1,2∨P2,1)B1,1 R6与消去 R8 ¬B1,1¬(P1,2∨P2,1) 逆否命题逻辑等价 R9 ¬(P1,2∨P2,1) R4/R8分离规则 R10(结果) ¬P1,2∧¬P2,1 迪摩根定律

50 基于电路的智能体 基于电路的智能体的目的：把对现状的感知变为智能体的行动 感知=input → 判断/行动
第3章 逻辑系统 基于电路的智能体 基于电路的智能体的目的：把对现状的感知变为智能体的行动 感知=input → 判断/行动 判断：尖叫→怪兽wumpus将死亡 行动：金光→抓起金子/行动控制=寄存器 Scream   Alive 延迟 glitter grab

51 第3章 逻辑系统 wumpus世界中智能体的判断(1) 位置判断：在L1,1—分为3种情况：一直留在[1,1]，从[1,2]走到[1,1]，从[2,1]走到[1,1] 使用位置寄存器/状态寄存器 forward ∨ ∧ bump L1,2 ∧ ∨ L1,1 facing-left L2,1 ∧ facing-down

52 wumpus世界中智能体的判断(2) 上述电路图表示为逻辑表达式 前述电路的逻辑表达式
第3章 逻辑系统 wumpus世界中智能体的判断(2) 上述电路图表示为逻辑表达式 前述电路的逻辑表达式 判断wumpus是否活着 发现金子后的行动 但因为没有变量，不能表示更一般的情况，如不同位置用同一个逻辑式

53 3.4 逻辑智能体的推理策略 逻辑智能体构造 Horn子句 置换与合一 前向链接算法 / 后向链接算法
第3章 逻辑系统 3.4 逻辑智能体的推理策略 逻辑智能体构造 Horn子句 置换与合一 前向链接算法 / 后向链接算法

54 逻辑智能体的构造(1) 以一阶谓词演算为核心的逻辑系统是典型的逻辑智能体
第3章 逻辑系统 逻辑智能体的构造(1) 以一阶谓词演算为核心的逻辑系统是典型的逻辑智能体 系统的基础是一阶语言，由此构造知识库 / 一般构造知识库(知识工程)的过程包括： 确定任务 收集相关知识 确定谓词、函数和常量词汇表

55 逻辑智能体的构造(2) 如果采用一阶语言的特殊形式—确定子句Horn子句，可获得高效推理 对领域(论域)的通用知识进行编码
第3章 逻辑系统 逻辑智能体的构造(2) 对领域(论域)的通用知识进行编码 对特定问题实例的描述进行编码 查询提交、推理、给出答案 调试知识库 如果采用一阶语言的特殊形式—确定子句Horn子句，可获得高效推理

56 Horn子句 Horn子句(Horn Clause)：是一类至多只有一个正文字的子句(子句=文字的析取式)
第3章 逻辑系统 Horn子句 Horn子句(Horn Clause)：是一类至多只有一个正文字的子句(子句=文字的析取式) 例子: ¬A∨¬B∨C (注意：这是一般公式AB→C的变形) Horn子句称为确定子句, 其中正文字称为子句的头, 负文字构成子句的体

57 Horn子句的性质 只有一个正文字的约束具有重要意义: 最重要的是最后一个性质
第3章 逻辑系统 Horn子句的性质 只有一个正文字的约束具有重要意义: 每个Horn子句实际上都是一个蕴涵式的变形, 实际知识库中常常使用这样易懂的形式 / 没有正文字的Horn子句可以写成结论为FALSE的蕴涵式 Horn子句的推理可以使用前向链接和后向链接算法 用Horn子句判定蕴涵所需时间与数据库成线性关系 最重要的是最后一个性质

58 推理策略 简要介绍2种推理算法—简单的前向链接算法和简单的后向链接算法,结合一个例子说明算法的应用
第3章 逻辑系统 推理策略 简要介绍2种推理算法—简单的前向链接算法和简单的后向链接算法,结合一个例子说明算法的应用 一阶推理规则—一般化分离规则(Generalized Modus Ponens) 对于原子语句pi, pi’, q, 存在置换,使得(pi)= (pi’), 对所有i都成立, 则

59 第3章 逻辑系统 置换与合一 置换(或代换)：设x1～xn是n个变量，且各不相同，t1～tn是n个项(常量、变量、函数)，ti≠xi，则有限序列{t1/x1, t2/x2 …tn/xn}称为一个置换 置换乘积(合成)：设和是2个置换，则先后作用于公式或项，称为置换乘积，用表示。 通过相关的置换,使不同的一阶公式成为一样的，这个过程称为合一

60 第3章 逻辑系统 合一置换 合一置换：设有一组谓词公式{E1～Ek}和置换，使E1=E2=…=Ek,则称为合一置换，E1～Ek称为可合一的 / 合一置换也叫通代 最一般合一置换(最广通代)：如果和都是公式组{E1～Ek}的合一置换，且有置换存在，使得=，则称为公式组{E1～Ek}的最一般合一置换，记为mgu (most general unification)

61 置换与合一的例子 有子句 则做置换 ={x/John}, 用一般化分离规则可得: q=Evil(John)
第3章 逻辑系统 置换与合一的例子 有子句 x King(x)∧ Greedy(x)→ Evil(x) King(John) Greedy(John) 则做置换 ={x/John}, 用一般化分离规则可得: q=Evil(John)

62 合一结果 对于合一UNIFY, 合一的结果是一个置换, 如: 详细的合一算法将在第6章介绍
第3章 逻辑系统 合一结果 对于合一UNIFY, 合一的结果是一个置换, 如: UNIFY(Know(John, x), Know(John, Jane)) ={x/Jane} UNIFY(Know(John, x), Know(y, Mary)) ={x/Mary, y/John} 但是UNIFY(K(John, x), K(x, Jane))=FAIL, 原因是x不能同时选取2个值 详细的合一算法将在第6章介绍

63 第3章 逻辑系统 用于逻辑推理的例子 问题描述: 美国法律规定：美国人(American)卖武器(weapon)给敌对国家(hostile)是犯罪的(criminal). 美国的敌国Nono有一些导弹(missile)，所有这些导弹是West上校卖给他们的，而West上校是一个美国人 证明：West是犯罪的

64 问题用一阶子句表示(1) 用确定子句表示上述内容 美国人卖武器给敌对国家是犯罪的
第3章 逻辑系统 问题用一阶子句表示(1) 用确定子句表示上述内容 美国人卖武器给敌对国家是犯罪的 American(x) ∧ Weapon(y) ∧ Sell(x,y,z) ∧ Hostile(z) → Criminal(x) [1] Nono有一些导弹 x Own(Nono, x) ∧ Missile(x) 消去其中的存在量词，引入新常量，得到2个原子公式(正文字) Own(Nono, M1) [4] Missile(M1) [5]

65 第3章 逻辑系统 问题用一阶子句表示(2) 所有该国导弹都是West上校出售的 Missile(y) ∧ Own(Nono, y)→Sell(West, y, Nono) [2] 导弹是武器 Missile(y) → Weapon(y) [3] 其它陈述： 美国人West American(West) [6] 敌国 Nono Hostile(Nono) [7] 上述描述放入知识库：[1]~[3]为确定子句(上述原始形式均可以化为原子的析取且只有一个正文字)， [4]~[7]为正文字

66 前向链接算法的说明(1) 前向链接算法的推理过程：
第3章 逻辑系统 前向链接算法的说明(1) 前向链接算法的推理过程： 从已知事实(知识库中的原子公式)开始，依次对知识库中的规则(以确定子句的形式出现)进行置换，检查规则前提部分的文字是否全部与知识库中的事实相匹配 如果是匹配的，则把该条规则已经做过置换的结论部分添加到知识库中，如果这个结论和查询(既需要推导出的结论)一致，则推理结束，获得证明

67 前向链接算法的说明(2) 约束：要求每次加入知识库的结论都是全新的，而不是已知事实的重命名(即谓词相同只是变量名不同)
第3章 逻辑系统 前向链接算法的说明(2) 重复上述过程，直到获得证明；或者再没有新的事实(推出的结论)加入，则此时推理以证明失败结束 约束：要求每次加入知识库的结论都是全新的，而不是已知事实的重命名(即谓词相同只是变量名不同)

68 简单的前向链接算法 第3章 逻辑系统 Function FC(KB,α) Return a substitution or FALSE
Inputs: KB , a set of first-order definite clauses / , the query = an atom local variables : new, the new rules inferred on each iteration repeat until new is empty new←{} for each rule r (in the form of define clause) in KB do for each  such that (p1∧…∧pn)= (p1’∧…∧pn’) get (q)=q’ if q’ is new (satisfied the constraint) then do add q’ to new ←UNIFY(q’, ) If  is not fail then return  add new to KB return false

69 前向链接算法例子(1) 使用前向链接算法对前面的例子进行推理 第一次循环体执行：
第3章 逻辑系统 前向链接算法例子(1) 使用前向链接算法对前面的例子进行推理 用知识库中的事实(即[4]~[7])依次对知识库中的各个子句进行置换操作并用推理规则获得新的文字 第一次循环体执行： 子句[1]前提部分未获满足(为什么？) 子句[2]—使用置换{x/M1}, 则可得 Sell(West, M1, Nono) [8] 子句[3]—使用置换{x/M1}，则可得Weapon(M1) [9]

70 前向链接算法例子(2) 第二次循环体执行： 此时new中为[8][9]，为原知识库所未有，将它们添加到知识库中 再次循环时new首先清空
第3章 逻辑系统 前向链接算法例子(2) 此时new中为[8][9]，为原知识库所未有，将它们添加到知识库中 第二次循环体执行： 再次循环时new首先清空 子句[1]—置换{x/West, y/M1, z/Nono} 得到Criminal(West) [10] 添加到new中，与查询进行合一测试，一致则返回 / 算法结束

71 前向链接生成的证明树 第3章 逻辑系统 Criminal(West) Weapon(M1) Sells(West,M1,Nono)
Hostile(Nono) American(West) Missile(M1) Owns(Nono,M1) Enemy(Nono,America)

72 反向链接算法的说明(1) 原始查询(既要证明的结论)以目标列表的形式出现，开始时列表中只有一个元素
第3章 逻辑系统 反向链接算法的说明(1) 原始查询(既要证明的结论)以目标列表的形式出现，开始时列表中只有一个元素 列表的操作相当于栈，是一个递归过程(如下)即深度优先的搜索过程 推理过程是从结论(子句的头)开始，找到匹配的头就扩展这个头所在的规则体；扩展部分又作为头继续扩展，直到全部原子均与事实相匹配 比较：正向=事实结论/反向=结论事实

73 反向链接算法的说明(2) 算法的推理过程是： 注意：事实是指有头没有体的子句(正文字)
第3章 逻辑系统 反向链接算法的说明(2) 算法的推理过程是： 选取栈当中的第一个目标，在知识库中寻找子句的头(即结论部分)能与目标合一的每个子句 每个这样的子句创建了一个递归调用过程，在这个递归调用过程中子句的前提(子句的体)被加入到目标栈当中 当栈中所有目标都得到匹配，则当前的证明分支是成功的 注意：事实是指有头没有体的子句(正文字)

74 反向链接算法的说明(3) 在算法中answers作为存放置换的数据结构，返回一系列置换操作，这些操作说明了反向链接算法获取证明的过程
第3章 逻辑系统 反向链接算法的说明(3) 在算法中answers作为存放置换的数据结构，返回一系列置换操作，这些操作说明了反向链接算法获取证明的过程 在算法中包括了置换的合成’(或者写为Compose(’,))，其效果就是依次进行每个置换

75 第3章 逻辑系统 反向链接算法的说明(4) 第一次应用算法，对于待证明的目标来说，本身就是一个正文字，此时要用这个文字中的常量对合适的规则(子句的头与该文字匹配)进行置换 这个置换通过递归调用带入下一次置换，就得到了合成置换 在本例中有：初始{x/West} 递归{x/West, y/M1} 递归{x/West, y/M1, z/Nono}

76 第3章 逻辑系统 简单的反向链接算法 Function BC(KB, goals, ) returns a set of substitutions Inputs: KB, goals=a list of conjuncts forming a query ( already applied),  =the current substitution (initial={}) local variables: answers=a set of substitutions (initial={}) if goals is empty then return {} q’=(FIRST(goals)) (初始为空，递归以后不空) for each rule r (in the form of define clause) in KB and ’=UNIFY(q, q’) succeeds new_goal={p1’, … , pn’} as REST(goals) answers=BC(KB, new_goal, ’))∪answers return answers

77 反向链接算法例子(1) 反向链接算法推理过程
第3章 逻辑系统 反向链接算法例子(1) 反向链接算法推理过程 目标Criminal(West)分解为公式[1]前提部分的4个文字，即American(West), Weapon(y), Sell(West, y, z), Hostile(z)—置换={x/West} American(West)和事实相匹配 需要递归匹配：Weapon(y), Sell(West, y, z), Hostile(z) Weapon(y)递归调用前={x/West}，进入第一次递归产生Missile(M1)，此时置换{y/M1}匹配，递归返回复合={x/West, y/M1}

78 第3章 逻辑系统 反向链接算法例子(2) 再次递归调用Sell(West, M1, z)—得到置换={z/Nono}，递归返回复合置换{x/West, y/ M1, z/Nono} 在置换过程中每个变量只能置换一个常量作为约束，减少置换的不定性 此时子目标全部匹配，再无新的子目标生成，返回置换集合结束

79 反向链接生成的证明树 第3章 逻辑系统 Criminal(West) American(West) Weapon(y)
Sells(West,M1,z) Hostile(Nono) Missile(y) Missile(M1) Owns(Nono ,M1) Enemy(Nono,Amerca) {} z/Nono {y/M1}

80 正向链接和反向链接 前向链接算法特点：数据驱动 / 是可靠的和完备的
第3章 逻辑系统 正向链接和反向链接 前向链接算法特点：数据驱动 / 是可靠的和完备的 后向链接算法特点：目标驱动 / 是可靠的但不是完备的(书中p220/p224) 可以从“是否能找到问题的解”角度考虑不完备性 后向链接算法根据目标来进行相关事实的匹配，对于大规模的知识库来说有助于减小搜索空间

81 参考书目 Stuart Russell / Peter Norvig: AIMA 第7章 /第8章 /第9章
第3章 逻辑系统 参考书目 Stuart Russell / Peter Norvig: AIMA 第7章 /第8章 /第9章 陆汝钤 编著: 人工智能(上册) 第1章 陆钟万，面向计算机科学的数理逻辑，科学出版社，1998年1月第1版 朱梧[木贾]、肖奚安，数理逻辑引论，南京大学出版社，1995年5月第1版 王元元，计算机科学中的逻辑学，科学出版社，1989年9月第1版

82 附录 形式系统简介 F1 形式系统和形式推演 F2 形式系统的语义 F3 形式系统的整体特征
第3章 逻辑系统 附录 形式系统简介 F1 形式系统和形式推演 F2 形式系统的语义 F3 形式系统的整体特征

83 第3章 逻辑系统 F1 形式系统定义和形式推演

84 形式系统定义(1) 逻辑的形式系统的定义 – 一个形式系统Formal System由5个部分组成：
第3章 逻辑系统 形式系统定义(1) 逻辑的形式系统的定义 – 一个形式系统Formal System由5个部分组成： (1)符号表，非空集合，即形式语言(如Lp和L)； (2)上全体符号的集合*的一个子集TERM，其元素称为FS的项；TERM有子集VARIABLE，其元素称为变量； (3)*的一个子集FORMULA，其元素称为FS的公式；FORMULA有子集ATOM，其元素称为原子公式；TERMFORMULA=；

85 形式系统定义(2) 其中、TERM、FORMULA称为FS的组成部分，AXIOM、RULE称为FS的推演部分
第3章 逻辑系统 形式系统定义(2) (4)FORMULA的一个子集AXIOM，其元素称为FS的公理； (5)FORMULA上的n元关系集合RULE，其元素称为FS的推理规则。 其中、TERM、FORMULA称为FS的组成部分，AXIOM、RULE称为FS的推演部分 公理推演系统包括AXIOM，而自然推演系统只包括推理规则

86 对象语言和元语言(1) 对象语言和元语言：作为被研究对象的语言称为对象语言，用以研究对象语言的语言称为元语言
第3章 逻辑系统 对象语言和元语言(1) 对象语言和元语言：作为被研究对象的语言称为对象语言，用以研究对象语言的语言称为元语言 例子：用汉语研究英语语法，则英语是对象语言，汉语是元语言 数理逻辑中的形式系统各有其自身的形式语言如Lp和L，这些是被研究的对象，因而是对象语言；但为了研究这些形式系统，又必须使用某种语言，那么这种语言便是元语言

87 对象语言和元语言(2) 形式系统的对象语言，其中的符号既是对客观对象的抽象，用于研究客观对象;同时又是一种符号客体，是被研究的对象
第3章 逻辑系统 对象语言和元语言(2) 如：“鸟正在飞翔”—描述—对象语言；“命题‘鸟正在飞翔’真”—对上句的评论—元语言。 形式系统的对象语言，其中的符号既是对客观对象的抽象，用于研究客观对象;同时又是一种符号客体，是被研究的对象

88 对象语言和元语言(3) 形式系统的元语言包括： 对形式系统中组成成分的称谓—项、公式、公理等 逻辑术语—如果-那么、当且仅当、存在、所有等
第3章 逻辑系统 对象语言和元语言(3) 形式系统的元语言包括： 对形式系统中组成成分的称谓—项、公式、公理等 逻辑术语—如果-那么、当且仅当、存在、所有等 对形式系统性质（整体特征）的描述—如一致性、完备性、可判定性等，该部分最重要 元语言中使用的符号：自然语言（如汉语）和一些被引进的符号，如：├、|= 等 未经解释的形式语言可以没有含义，但元语言必须有其具体含义。

89 元理论 元理论是关于形式系统的理论，包括三部分内容：
第3章 逻辑系统 元理论 元理论是关于形式系统的理论，包括三部分内容： 关于形式系统语法(syntax)的研究，不涉及具体意义的符号体系，研究符号串的推演，即形式推演； 关于形式系统语义(semantics)的研究，研究形式系统在被作出各种解释时的性质； 关于形式系统语法和语义关系的研究，特别是形式系统的性质，如：合理性、完备性等。

90 形式推演 形式推演：定义了公式之间的形式可推演性关系，它涉及公式的语法结构，其正确性能够机械地证明
第3章 逻辑系统 形式推演 形式推演：定义了公式之间的形式可推演性关系，它涉及公式的语法结构，其正确性能够机械地证明 用记号├ 表示形式可推演关系，读作“推出” 用├ A表示A是由形式可推演的（或形式可证明的），其中是前提，A是结论 记号├不是形式语言中的符号， ├ A也不是形式语言中的公式，而是元语言中的命题

91 常用推演规则(1) 形式推演由形式推演的规则定义 命题逻辑中有一些常用的推演规则(规则模式)
第3章 逻辑系统 常用推演规则(1) 形式推演由形式推演的规则定义 命题逻辑中有一些常用的推演规则(规则模式) 肯定前提 if A∈ then ├ A (∈) 增加前提 if ├ A then  ,  ‘├ A (+) 自反 A├ A (Ref) 传递 if ├  ‘├ A then ├ A ()

92 常用推演规则(2) ￢消去(反证律) if  , ￢A├ B &  , ￢A├￢B then ├ A (￢-) ￢引入(归谬律)
第3章 逻辑系统 常用推演规则(2) ￢消去(反证律) if  , ￢A├ B &  , ￢A├￢B then ├ A (￢-) ￢引入(归谬律) if  , A├ B &  , A├ ￢B then ├ ￢A (￢+) →消去 if ├ A→B, ├ A then ├ B (→-) →引入 if , A ├ B then ├ A→B (→+)

93 常用推演规则(3) ∧消去 if ├ A∧B then ├ A, ├ B (∧-) ∧引入
第3章 逻辑系统 常用推演规则(3) ∧消去 if ├ A∧B then ├ A, ├ B (∧-) ∧引入 if ├ A, ├ B then ├ A∧B (∧+) ∨消去 if  , A├ C &  ,B├ C then  ,A∨B├ C (∨-) ∨引入 if ├ A then ├ A∨B, ├ B∨A (∨+)

94 常用推演规则(2) 通过连接词的增减或变形，实现公式的变换 常用A→B  AB ≡消去 if ├ A≡B, ├A then ├B
第3章 逻辑系统 常用推演规则(2) ≡消去 if ├ A≡B, ├A then ├B if ├ A≡B, ├B then ├A (≡－) ≡引入 if  , A├ B &  , B├ A then ├A≡B (≡+) 通过连接词的增减或变形，实现公式的变换 常用A→B  AB

95 第3章 逻辑系统 形式可推演性(1) (命题逻辑)形式可推演性：在命题逻辑中，A是由可形式推演的(或形式可证明的)，记为├A，当且仅当├A能通过有限次应用命题逻辑的形式推演规则生成 即├A成立，当且仅当存在有限序列使得 1├A1，2├A2，…，n├An 中的每一项均由某个形式推导规则生成,且n├An 就是├A即n=,An=A

96 形式可推演性(2) 用 A表示├A不成立 用A|-|B表示左右两边的公式可以互相推出，称其为语法等值公式或等值公式
第3章 逻辑系统 形式可推演性(2) 用 A表示├A不成立 用A|-|B表示左右两边的公式可以互相推出，称其为语法等值公式或等值公式 建立在上述形式推演规则基础上的形式推演系统称为自然推演(演绎)系统

97 形式可推演性(3) 命题逻辑中的形式推演规则都包括在一阶逻辑当中，但是其中出现的公式是一阶语言中的公式，另外增加了关于量词的规则
第3章 逻辑系统 形式可推演性(3) 命题逻辑中的形式推演规则都包括在一阶逻辑当中，但是其中出现的公式是一阶语言中的公式，另外增加了关于量词的规则 (一阶逻辑)形式可推演性：在一阶逻辑中，A是由可形式推演的(或形式可证明的)，记为├A，当且仅当├A能通过有限次应用一阶逻辑的形式推演规则生成 形式推演的例子可以参考本章后面列出的3本关于逻辑的教科书

98 第3章 逻辑系统 F2 形式系统的语义

99 形式系统的语义(1) 语义即对形式语言进行解释
第3章 逻辑系统 形式系统的语义(1) 语义即对形式语言进行解释 研究可推导性即形式推演(├)时不考虑作为前提和结论的命题的内容，只考虑命题真假并由此确定前提的真是否蕴涵结论的真，即前提和结论之间是否有可推导关系(语法) 研究形式系统的语义时，对形式系统赋予研究对象的集合即论域；用论域中的个体对象、对象之上的运算(函数)、对象之间的关系(谓词)去解释形式系统中的符号，称作指称denote  指称语义学

100 第3章 逻辑系统 形式系统的语义(2) 赋予形式系统的论域及解释称为形式系统的语义结构，简称结构(structure)/ 结构及其在该结构下公式所取真值的规定，称为形式系统的指称语义(denotational semantics)

101 命题逻辑的可满足性 研究命题逻辑的语义，即研究公式(公式集)的真假赋值问题
第3章 逻辑系统 命题逻辑的可满足性 研究命题逻辑的语义，即研究公式(公式集)的真假赋值问题 真假赋值：真假赋值是以所有命题符号的集合为定义域，以真假值{1,0}为值域的函数。真假赋值v给公式A指派的值记作Av 可满足性：是可满足的，当且仅当有真假赋值v，使得v=1。此时称v满足。

102 第3章 逻辑系统 可满足性 的可满足性蕴涵了中所有公式的可满足性，但反过来不成立。因为这要求同一个真假赋值满足所有的公式(并非所有可满足的公式使用同一个赋值) 重言式和矛盾式 A是重言式(永真式)，当且仅当对于任意的真假赋值v，Av=1 A是矛盾式(永假式)，当且仅当对于任意的真假赋值v，Av=0

103 真假判断与逻辑推论 一个命题公式是重言式或者是矛盾式或者两者都不是，需要进行判定。判定方法可通过构造真假值表方法或采用树形分支的方法来判定
第3章 逻辑系统 真假判断与逻辑推论 一个命题公式是重言式或者是矛盾式或者两者都不是，需要进行判定。判定方法可通过构造真假值表方法或采用树形分支的方法来判定 可推导关系研究前提的真是否蕴涵结论的真，引入语义以后对公式进行真假赋值；如果对任意的真假赋值，都有上述关系，则说明前提和结论之间存在一种逻辑推论关系(或称逻辑蕴涵)。此时对关系陈述得也更精确

104 第3章 逻辑系统 命题逻辑的逻辑推论 逻辑推论：设、A分别是命题逻辑中的公式集合和公式,A是的逻辑推论，记为 A，当且仅当对于任意真假赋值v，v=1蕴涵Av=1。 |=可读作“逻辑地蕴涵”，|=是前提和结论A之间的关系,但不是命题语言中的符号，|=A是元语言中的命题

105 逻辑推论的证明 逻辑推论的证明 要证明|=A时，即要证明对于任何真假赋值v，如果v=1则Av=1 但任意的真假赋值难于验证
第3章 逻辑系统 逻辑推论的证明 逻辑推论的证明 要证明|=A时，即要证明对于任何真假赋值v，如果v=1则Av=1 但任意的真假赋值难于验证 故使用反证法，假设|≠A，即存在一个真假赋值v，使得v=1且Av=0，由此而产生矛盾，即肯定了 |=A

106 第3章 逻辑系统 一阶语言的语义(1) 一阶语言的语义：一阶语言的解释包括一个论域和一个函数，函数把一阶语言中的个体符号、n元关系符号(即谓词)、m元函数符号分别映射到论域中的个体、论域上的n元关系和m元全函数，是在这个论域中对一阶语言的解释

107 第3章 逻辑系统 一阶语言的语义(2) 如果n元关系符号和m元函数中不含自由变量，其项为论域中的个体ai，则原子公式F(t1,…,tn)被解释为：a1,…,an有R关系；项f(t1,…,tn)被解释为论域中的个体f(a1,…,an) 对于含有自由变量的函数(项)和公式，则分别被解释为论域上的m元函数和n元命题函数，它们经过解释，再给其中的自由变量符号指派论域中的某些个体，就得到论域中个体作为其值、真或假的命题作为其真假值

108 第3章 逻辑系统 一阶语言的赋值(1) 赋值：一阶语言L的赋值v包括一个论域和一个函数，记作v，以L中所有个体符号a、关系符号F、函数符号f和自由变量符号u构成的集合为定义域，且分别把v(a)、v(F)、v(f)、v(u)写作av、Fv、fv、uv，则有 (1)av, uv∈D (2)FvDn (3)fv: Dm→D

109 一阶语言的赋值(2) 项的值：在以D为论域的赋值v之下的项的值递归定义如下： 对于一阶语言的项t，设v是以D为论域的赋值，则tv∈D
第3章 逻辑系统 一阶语言的赋值(2) 项的值：在以D为论域的赋值v之下的项的值递归定义如下： (1)av, uv∈D (2)f(t1,…,tn)v=fv(t1v,…,tnv) 对于一阶语言的项t，设v是以D为论域的赋值，则tv∈D

110 一阶逻辑的逻辑推论 公式的真假值：一阶语言的公式在以D为论域的赋值之下，其真假值可以递归定义
第3章 逻辑系统 一阶逻辑的逻辑推论 公式的真假值：一阶语言的公式在以D为论域的赋值之下，其真假值可以递归定义 一阶逻辑的逻辑推论: 与命题逻辑相同，只是这里不使用真假赋值，而用赋值 逻辑推论：设、A分别是一阶语言的公式集和公式，A是的逻辑推论，记作|=A，当且仅当对于任何赋值v，v=1蕴涵Av=1

111 第3章 逻辑系统 逻辑推论的证明方法 一阶逻辑的逻辑推论证明方法类似于命题逻辑，常用反证法。但对于否证逻辑推论，则需要构造赋值所需的论域。确定论域时，关键在于论域的大小

112 第3章 逻辑系统 F3 形式系统的整体特征

113 形式系统的整体特征 在经典逻辑的形式系统中，形式推演是语法概念，逻辑推论是语义概念
第3章 逻辑系统 形式系统的整体特征 在经典逻辑的形式系统中，形式推演是语法概念，逻辑推论是语义概念 形式系统的整体特征：是在形式系统引入语义以后，研究对于任何一阶语言的公式集和公式A在何种赋值的条件下，其结果是否为真 / 研究形式推演与逻辑推论间的关系 赋值的条件： 给定某个赋值—可满足性 给定任意赋值—有效性

114 可靠性定理与完备性定理 对于任何一阶语言的公式集和公式A，
第3章 逻辑系统 可靠性定理与完备性定理 对于任何一阶语言的公式集和公式A， ├ A|=A表示：凡是形式可推演性所反映的前提和结论之间的关系，在非形式的推理中都是成立的，即形式可推演性对于反映非形式的推理是可靠的，此即可靠性定理(或者称合理性) |=A ├ A表示：凡是在非形式推理中成立的前提和结论之间的关系，形式可推演性都是能够反映的，即形式可推演性在反映非形式推理时没有遗漏，此即完备性定理

115 可满足性与有效性(1) 下面给出有关定义和定理，但均不加证明
第3章 逻辑系统 可满足性与有效性(1) 下面给出有关定义和定理，但均不加证明 可满足性—一阶逻辑公式集合是可满足的，当且仅当有(以某个不空集为论域)赋值v，使得v=1 / 当v=1时，称v满足 反过来，不可满足性就是对任意论域上的任意赋值都有v=0

116 可满足性与有效性(2) 有效性：一阶逻辑公式A是有效的，当且仅当对于(以任何不空集为论域)任何赋值v，Av=1 / 有效性也称为普遍有效性
第3章 逻辑系统 可满足性与有效性(2) 有效性：一阶逻辑公式A是有效的，当且仅当对于(以任何不空集为论域)任何赋值v，Av=1 / 有效性也称为普遍有效性 论域中的可满足性、有效性： (1)在D中是可满足的，当且仅当有以D为论域的赋值v，使得v=1 (2)A在D中是有效的，当且仅当对于任何以D为论域的赋值v，Av=1

117 可满足性与有效性(3) (关于命题的)定理: (1)A是可满足的，当且仅当¬A是不有效的；(2)A是有效的，当且仅当¬A是不可满足的。
第3章 逻辑系统 可满足性与有效性(3) (关于命题的)定理: (1)A是可满足的，当且仅当¬A是不有效的；(2)A是有效的，当且仅当¬A是不可满足的。 (关于一阶的)定理: (1)A(u1,…,un)是可满足的，当且仅当x1... xn A(x1,…,xn)是可满足的 (2)A(u1,…,un)是有效的，当且仅当x1... xn A(x1,…,xn)是有效的

118 可满足性与有效性(4) 定理: 设Form(L)，A∈Form(L)，和A不含相等符号，D和D1是论域，且|D|≤|D1|，则
第3章 逻辑系统 可满足性与有效性(4) 定理: 设Form(L)，A∈Form(L)，和A不含相等符号，D和D1是论域，且|D|≤|D1|，则 (1)如果在D中是可满足的，则在D1中是可满足的； (2)如果A在D1中是有效的，则在D中是有效的

119 可靠性定理(1) 可靠性定理[1]：设Form(L)，A∈Form(L)(也包括了命题语言Lp) (1)如果├A，则|=A；
第3章 逻辑系统 可靠性定理(1) 可靠性定理[1]：设Form(L)，A∈Form(L)(也包括了命题语言Lp) (1)如果├A，则|=A； (2)如果├A，则|=A(即所有形式可推演的都是有效的)

120 可靠性定理(2) 协调性： Form(L)是协调的，当且仅当不存在A ∈Form(L)，使得├A且├ ¬A
第3章 逻辑系统 可靠性定理(2) 协调性： Form(L)是协调的，当且仅当不存在A ∈Form(L)，使得├A且├ ¬A 可靠性定理[2]：设Form(L)，A∈Form(L) (1)如果是可满足的，则是协调的； (2)如果A是可满足的，则A是协调的。 上述2个定理是等价的，即用可满足性和协调性来陈述可靠性

121 完备性定理(1) 命题逻辑的完备性 定理[1]：设 Form(Lp)，A∈Form(Lp) (1)如果是协调的，则是可满足的；
第3章 逻辑系统 完备性定理(1) 命题逻辑的完备性 定理[1]：设 Form(Lp)，A∈Form(Lp) (1)如果是协调的，则是可满足的； (2)如果A是协调的，则A是可满足的。 定理[2]：设 Form(Lp)，A∈Form(Lp) (1)如果|=A，则├ A； (2)如果|=A，则├ A(所有重言式都是形式可证明公式)

122 完备性定理(2) 一阶逻辑的完备性 定理[1]:设 Form(L)，A∈Form(L) (1)如果是协调的，则是可满足的；
第3章 逻辑系统 完备性定理(2) 一阶逻辑的完备性 定理[1]:设 Form(L)，A∈Form(L) (1)如果是协调的，则是可满足的； (2)如果A是协调的，则A是可满足的。 定理[2]:设 Form(L)，A∈Form(L) (1)如果|=A，则├ A； (2)如果|=A，则├ A(所有有效公式都是形式可证明公式)。 如果对论域限定以后，可得更精确的陈述