1、 3.1 命题逻辑和一阶谓词逻辑3.2 逻辑系统的语法和语义3.3 逻辑推理举例3.4 逻辑智能体的推理策略参考书目附录 形式系统简介第3章 逻辑系统3 AI研究内容之一是推理,即研究怎样使计算机获得自动推理的能力 数理逻辑用数学方法研究各种推理中的逻辑问题,以推理本身作为研究对象 AI要使用逻辑推理,就必然涉及数理逻辑 / 数理逻辑的经典部分经典的命题逻辑和一阶谓词逻辑,同时作为人工智能的知识表示方法和推理方法而存在;因此数理逻辑是人工智能的一个基础第3章 逻辑系统4 基于知识的智能体的核心部件是知识库,当这些知识以逻辑形式表示并进行相应的推理时,就是逻辑智能体 知识表示:命题逻辑、一阶谓词
2、逻辑 推理(一阶谓词逻辑)主要有3类推理算法:前向链接和演绎系统、反向链接和逻辑程序设计(本章)、归结反演和定理证明系统(第4章) 采用命题和谓词演算进行推理的系统(如演绎系统)是一种典型的逻辑智能体第3章 逻辑系统3.1 命题逻辑和一阶谓词逻辑命题、真值、原子公式、合式公式谓词、论域、个体量词、变量、函数一阶语言、一阶语言的项第3章 逻辑系统6 命题:描述客观世界的可区分真假的陈述句, 即判断(经典二值逻辑:非真即假) 是命题的例子: 2+2=4 / 二月份有30天 / 2002年哈尔滨有地震 / 人类能够证明数论中所有论断非真即假(有待时间) 不是命题的例子: 张三比李四聪明 / 公共汽车
3、内非常拥挤(各人认识不同)第3章 逻辑系统7 命题变量(变元):一个命题用符号表示,称为命题符号 当命题符号代表任一个命题时,即为命题变量 真值:真或假 一个命题或命题变量具有真值 真值连接词(5个):否定/合取/析取/蕴涵/等价第3章 逻辑系统8 真值函数:真值联结词可以视为一元或二元映射(真值函数),是从T,F到T,F,其余是T,F2到T,F的映射 / 其函数定义由真值表确定 简单命题:一个被视为整体的、具有真或假的命题是简单命题; 复合命题:使用联结词将简单命题联结起来的命题是复合命题第3章 逻辑系统9 命题逻辑:研究复合命题之间的推导关系 命题语言:是命题逻辑使用的形式语言,是符号的集
4、合,用Lp表示 / 包括:命题符号、连接词、左右括号 原子公式:命题语言中的一个表达式是原子公式,当且仅当它是一个命题符号 / 原子公式也称为文字(包括正文字和负文字)第3章 逻辑系统10 合式公式(well-formed formula),简称公式,记作wff:一个表达式是一个公式,当且仅当它能通过有限次地使用下述步骤生成:(1)原子公式是公式;(2)如果A是公式,则(A)是公式;(3)如果A、B均为公式,则A*B是公式,其中*表示中的任意一个 / 公式的形成规则 / 命题逻辑的主要研究对象是公式第3章 逻辑系统11 从命题到一阶谓词:命题内部逻辑结构的分解 对判断的分解,把判断中的具体内容
5、抽出,称为个体;剩下的判断即为谓词 谓词可看作是从个体域或个体域的笛卡儿乘积到真值集合T/F的映射 典型的推理例子:(1)凡人皆有死;(2)苏格拉底是人;(3)苏格拉底有死。(三段论式)M(x)D(x), M(s) D(s)第3章 逻辑系统12 论域和个体:在一阶逻辑中,被研究对象构成的非空集称为论域;论域中的每个元素称为个体 论域例子:前面例子中的论域是“人” / 所有的有理数都是实数:其论域为有理数 一阶逻辑还研究个体之间的关系(或个体的性质)及作用于个体的函数 论域/个体/个体间关系/作用于个体函数 这4个成分构成了一阶逻辑的结构第3章 逻辑系统13 谓词(关系):一阶形式语言中用于指称
6、论域中个体的性质或者个体之间关系的形式符号(大写字母表示) 给定了论域,就确定了谓词的真假值 一元谓词:个体的性质;二元谓词(多元谓词):个体的关系 个体的位置空位,具体化构成意义完整的语句 空位的数目谓词的元数几元谓词第3章 逻辑系统14 变量(变元):表示论域内的任意一个个体 / 常量(常元),表示确定的个体 量词与变量:量词用来表示谓词的判断特性 全称量词:对所有的x x P(x) 存在量词:存在x x P(x) 约束变量:、中x的变量,量词所管辖的公式如P(x)称为量词辖域 自由变量:不在量词辖域内的变量为自由变量第3章 逻辑系统15 区别:自由变量可代入常量,约束变量不行,因为a P
7、(a)无意义 ;约束变量可改名,自由变量不行 带有全称变量x的命题表示为一阶公式时,其表示形式为 x(P(x),带有存在变量x的命题则表示形式为x(P(x) 例子:所有有理数都是实数 x(P(x)R(x),有些人身高超过2米x(M(x)G(x) 上述使用方式不可改变,否则造成逻辑错误第3章 逻辑系统16 函数:表示个体之间的运算,可作用于一个或数个个体(用小写字母) 给定一个或若干个体(对象),产生一个新的个体(对象)/ 函数的元数 例子:x的父亲 father(张三) 两数之和仍是一个数 add(e1, e2)第3章 逻辑系统17 谓词和函数的区别:谓词代表语句,结果是关系(具有真假值);函
8、数代表关系运算,结果是一个新个体 例子:谓词SUM(e1, e2, e3) 说明e1、e2、e3之间的关系是e1与e2的和是e3 , 函数add(e1, e2)说明e1与e2相加的结果仍是一个数第3章 逻辑系统18 一阶语言L:是一阶逻辑使用的形式语言,可以和任何结构(论域)没有联系,也可以与某个结构有联系 与结构没有联系的一阶语言由8类符号组成:(1)无限序列的个体符号(个体常量)(2)无限序列的谓词符号,有确定的元数n1有一个特殊的谓词符号称为相等符号(等式),记为=。 L可含或不含=,如果含有,即称为含=的一阶逻辑第3章 逻辑系统19(3)无限序列的函数符号,有确定的元数m1(4)无限序
9、列的自由变量:用u/v/w等表示自由变量(5)无限序列的约束变量:用x/y/z等表示约束变量(6)联结词:(7)量词: 、(8)标点:左右括号、逗号 ( ) ,第3章 逻辑系统20 L的项:一阶语言中的一个符号是项t,当且仅当它能通过有限次使用下述步骤生成:(1)个体常量、自由变量是项;(2)如果t1tn是项,且f是n元函数,则f(t1tn)是项 L的原子公式:一阶语言中的一个表达式是一个原子公式,当且仅当它有如下2种形式:(1)F(t1tn),F是n元谓词,t1tn是项;(2)=(t1,t2)或t1=t2, t1、t2是项第3章 逻辑系统21 L的公式:一阶语言中的一个表达式是一个公式,当且
10、仅当它能通过有限次使用下述步骤生成:(1)原子公式是公式;(2)如果A是公式,则(A)是公式;(3)如果A、B均为公式,则A*B是公式,其中*表示中的任意一个(4)如果A(u)是公式,且x不在A(u)中出现,则x A(x)、x A(x)都是公式第3章 逻辑系统22 一阶谓词公式的例子 数学命题的表示: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) 或者 xy(H
11、(x,y)F(x)G(y) 第3章 逻辑系统3.2 逻辑系统的语法和语义逻辑系统的语法逻辑系统的语义语法和语义之间的关系第3章 逻辑系统24 逻辑系统(亦称形式系统Formal System)由5个部分组成: 符号表非空集合,即逻辑(形式)语言如一阶语言 上全体符号的集合*的子集项和变量 *的子集公式 | 公式和项的交集为空 公式FORMULA上的子集公理AXIOM 公式上的n元关系集合推理规则RULE 、项TERM、FORMULA称为FS的组成部分 / AXIOM、RULE称为FS的推演部分第3章 逻辑系统25 逻辑系统除符号表以外的部分构成了逻辑系统的语法 形式推演:定义了公式之间的形式可
12、推演性关系,它涉及公式的语法结构,其正确性能够机械地证明 用记号 表示形式可推演关系,读作“推出” 用 A表示A是由形式可推演的(或形式可证明的),其中是前提,A是结论第3章 逻辑系统26 形式推演由形式推演规则定义,举例如下: 自反A A (Ref) 传递if A then A () 消去(反证律)if , A B & , AB then A() 公式变换AB AB第3章 逻辑系统27 形式可推演性:在命题/一阶逻辑系统中,A是由可形式推演的(或形式可证明的),记为A,当且仅当A能通过有限次应用相应逻辑的形式推演规则生成 即A成立,当且仅当存在有限序列使得 1A1,2A2,nAn 中的每一项
13、均由某个形式推导规则生成,且nAn 就是A即n=,An=A 建立在上述形式推演规则基础上的形式推演系统称为自然推演(演绎)系统第3章 逻辑系统28 语义即对形式语言进行解释 研究可推导性即形式推演()时不考虑作为前提和结论的命题的内容,只考虑命题真假并由此确定前提的真是否蕴涵结论的真,即前提和结论之间是否有可推导关系(语法) 研究形式系统的语义时,对逻辑系统赋予研究对象的集合即论域;用论域中的个体对象、对象之上的运算(函数)、对象之间的关系(谓词)去解释逻辑系统中的符号,称作指称denote 指称语义学 赋予形式系统的论域及解释称为形式系统的语义结构,简称结构(structure)第3章 逻辑
14、系统29 研究命题逻辑的语义,即研究公式(公式集)的真假赋值问题 真假赋值:真假赋值是以所有命题符号的集合为定义域、以真假值1,0为值域的函数。真假赋值v给公式A指派的值记作Av 可满足性:是可满足的,当且仅当有真假赋值v,使得v=1。此时称v满足。第3章 逻辑系统30 的可满足性蕴涵了中所有公式的可满足性,但反过来不成立。因为这要求同一个真假赋值满足所有的公式(并非所有可满足的公式使用同一个赋值) 重言式和矛盾式 A是重言式(永真式),当且仅当对于任意的真假赋值v,Av=1 A是矛盾式(永假式),当且仅当对于任意的真假赋值v,Av=0第3章 逻辑系统31 一个命题公式是重言式或者是矛盾式或者
15、两者都不是,需要进行判定。判定方法可通过构造真假值表方法或采用树形分支的方法来判定 可推导关系:研究前提的真是否蕴涵结论的真,引入语义以后对公式进行真假赋值;如果对任意的真假赋值,都有上述关系,则说明前提和结论之间存在一种逻辑推论关系(或称逻辑蕴涵)第3章 逻辑系统32 逻辑推论:设、A分别是命题逻辑中的公式集合和公式,A是的逻辑推论,记为 A,当且仅当对于任意真假赋值v,v=1蕴涵Av=1。 |=可读作“逻辑地蕴涵”,|=是前提和结论A之间的关系 逻辑推论的证明 要证明|=A时,即要证明对于任何真假赋值v,如果v=1则Av=1 (通常使用反证法)第3章 逻辑系统33 一阶语言的语义:一阶语言
16、的解释包括一个论域和一个函数 函数把一阶语言中的个体符号映射到论域中的个体 n元关系符号(即谓词)映射到论域上的n元关系 m元函数符号映射到论域上的m元全函数 以上组成了该论域中对一阶语言的解释第3章 逻辑系统34 赋值:一阶语言L的赋值v包括一个论域D和一个函数(记作v) L中所有个体符号a为定义域,其赋值v(a)或av 关系符号F的赋值v(F)或Fv 函数符号f的赋值v(f)或fv 自由变量符号u的赋值v(u)或uv 则有(1)av, uvD(2)FvDn(3)fv: DmD第3章 逻辑系统35 公式的真假值:一阶语言的公式在以D为论域的赋值之下,其真假值可以递归定义 一阶逻辑的逻辑推论:
17、 与命题逻辑相同,只是这里不使用真假赋值,而用赋值 逻辑推论:设、A分别是一阶语言的公式集和公式,A是的逻辑推论,记作|=A,当且仅当对于任何赋值v,v=1蕴涵Av=1 一阶逻辑的逻辑推论证明方法类似于命题逻辑,常用反证法。但对于否证逻辑推论,则需要构造赋值所需的论域。确定论域时,关键在于论域的大小第3章 逻辑系统36 在经典逻辑的形式系统中,形式推演是语法概念,逻辑推论是语义概念 形式系统的整体特征:是在形式系统引入语义以后,研究对于任何一阶语言的公式集和公式A在何种赋值的条件下,其结果是否为真即研究形式推演与逻辑推论之间的关系 赋值的条件: 给定某个赋值可满足性 给定任意赋值有效性第3章
18、逻辑系统37 对于任何一阶语言的公式集和公式A, A|=A表示:凡是形式可推演性所反映的前提和结论之间的关系,在非形式的推理中都是成立的,即形式可推演性对于反映非形式的推理是可靠的,此即可靠性定理(或者称合理性) |=A A表示:凡是在非形式推理中成立的前提和结论之间的关系,形式可推演性都是能够反映的,即形式可推演性在反映非形式推理时没有遗漏,此即完备性定理第3章 逻辑系统38 不加证明地给出有关定义和定理 可满足性一阶逻辑公式集合是可满足的,当且仅当有(以某个不空集为论域)赋值v,使得v=1 / 当v=1时,称v满足 反过来,不可满足性就是对任意论域上的任意赋值都有v=0 第3章 逻辑系统3
19、9 有效性:一阶逻辑公式A是有效的,当且仅当对于(以任何不空集为论域)任何赋值v,Av=1 / 有效性也称为普遍有效性 论域中的可满足性、有效性:(1)在D中是可满足的,当且仅当有以D为论域的赋值v,使得v=1(2)A在D中是有效的,当且仅当对于任何以D为论域的赋值v,Av=1第3章 逻辑系统40 (关于命题的)定理: (1)A是可满足的,当且仅当A是不有效的;(2)A是有效的,当且仅当A是不可满足的。 (关于一阶的)定理: (1)A(u1,un)是可满足的,当且仅当x1. xn A(x1,xn)是可满足的 (2)A(u1,un)是有效的,当且仅当x1. xn A(x1,xn)是有效的第3章
20、逻辑系统41 可靠性定理1:设Form(L),AForm(L)(也包括了命题语言Lp)(1)如果A,则|=A;(2)如果A,则|=A(即所有形式可推演的都是有效的) 协调性(无矛盾性): Form(L)是协调的,当且仅当不存在A Form(L),使得A且 A 可靠性定理2:设Form(L),AForm(L)(1)如果是可满足的,则是协调的;(2)如果A是可满足的,则A是协调的。(12等价)第3章 逻辑系统42 命题逻辑和一阶逻辑的完备性 定理1:设 Form(L),AForm(L)(含Lp)(1)如果是协调的,则是可满足的;(2)如果A是协调的,则A是可满足的。 定理2:设 Form(L),A
21、Form(L)(1)如果|=A,则 A;(2)如果|=A,则 A(所有有效公式都是形式可证明公式)。 如果对论域限定以后,可得更精确的陈述第3章 逻辑系统3.3 逻辑推理举例 wumpus世界命题逻辑推理模式基于电路的智能体第3章 逻辑系统44 Wumpus是一个早期电脑游戏中的怪物 Agent感知: 陷阱旁边有微风breeze 怪兽旁边有恶臭stench 金子闪闪发光glitter 感觉墙的反弹 陷阱和怪物的位置随机生成第3章 逻辑系统stenchBreezePitWumpus(Monster)BreezeStenchGoldPitBreezestenchBreezeAgentBreezeP
22、itBreeze45 Wumpus世界搜索图示感知用5元组表示感知wumpus, 感知微风, 感知金光, 感知墙, 感知wumpus被杀死A=AgentB=BreezeG=Glitter,GoldOK=safe squareP=PitS=StenchV=visitedW=wumpusN=None1,42,43,44,41,32,33,34,31,2 OK2,23,24,21,1 A OK2,1 OK3,14,1第3章 逻辑系统1,42,43,44,41,32,33,34,31,2OK2,2P?3,24,21,1VOK2,1 ABOK3,1P?4,1 (a) N,N,N,N,N(b) N,B,N
23、,N,N461,42,43,44,41,3W!2,33,34,31,2 ASOK2,2OK3,24,21,1VOK2,1 BVOK3,1P!4,1第3章 逻辑系统1,42,4P?3,44,41,3W!2,3 AB S G3,3P?4,31,2 S VOK2,2VOK3,24,21,1VOK2,1 BVOK3,1P!4,1A=AgentB=BreezeG=Glitter,GoldOK=safe squareP=PitS=StenchV=visitedW=wumpusN=None (c) S,N,N,N,N (d) S,B,G,N,N47 只考虑陷阱的情况 Pi,j=T i,j中有陷阱,记为Pi,
24、j Bi,j=T i,j中有微风,记为Bi,j 规则如下: R1P1,1 R2B1,1P1,2P2,1 R3B2,1P1,1P2,2P3,1 R4B1,1 R5B2,1第3章 逻辑系统48 分离规则 与消去 逻辑等价(双向蕴涵消去), 第3章 逻辑系统()()()()49 用R1R5规则和推理模式证明:1,2和2,1中没有陷阱,即P1,2和P2,1 证明: 从R2开始 R6(B1,1(P1,2P2,1)(P1,2P2,1)B1,1)R2双向蕴涵消去 R7(P1,2P2,1)B1,1R6与消去 R8B1,1(P1,2P2,1)逆否命题逻辑等价 R9(P1,2P2,1)R4/R8分离规则 R10(
25、结果) P1,2P2,1迪摩根定律第3章 逻辑系统50 基于电路的智能体的目的:把对现状的感知变为智能体的行动 感知=input 判断/行动 判断:尖叫怪兽wumpus将死亡 行动:金光抓起金子/行动控制=寄存器第3章 逻辑系统grabglitterAlive延迟Scream 51 位置判断:在L1,1分为3种情况:一直留在1,1,从1,2走到1,1,从2,1走到1,1 使用位置寄存器/状态寄存器第3章 逻辑系统L1,2L2,1facing-leftfacing-downL1,1forwardbump52 上述电路图表示为逻辑表达式111,11,11111,21112,1()()()ttttt
26、tttttLLforwardbumpLfacingleftforwardLfacingdownforward 第3章 逻辑系统 前述电路的逻辑表达式 判断wumpus是否活着 发现金子后的行动 但因为没有变量,不能表示更一般的情况,如不同位置用同一个逻辑式1tttalivescreamalive ttglittergrab3.4 逻辑智能体的推理策略逻辑智能体构造Horn子句置换与合一前向链接算法 / 后向链接算法第3章 逻辑系统54 以一阶谓词演算为核心的逻辑系统是典型的逻辑智能体 系统的基础是一阶语言,由此构造知识库 / 一般构造知识库(知识工程)的过程包括: 确定任务 收集相关知识 确定
27、谓词、函数和常量词汇表第3章 逻辑系统55 对领域(论域)的通用知识进行编码 对特定问题实例的描述进行编码 查询提交、推理、给出答案 调试知识库 如果采用一阶语言的特殊形式确定子句Horn子句,可获得高效推理第3章 逻辑系统56 Horn子句(Horn Clause):是一类至多只有一个正文字的子句(子句=文字的析取式) 例子: ABC (注意:这是一般公式ABC的变形) Horn子句称为确定子句, 其中正文字称为子句的头, 负文字构成子句的体第3章 逻辑系统57 只有一个正文字的约束具有重要意义: 每个Horn子句实际上都是一个蕴涵式的变形, 实际知识库中常常使用这样易懂的形式 / 没有正文
28、字的Horn子句可以写成结论为FALSE的蕴涵式 Horn子句的推理可以使用前向链接和后向链接算法 用Horn子句判定蕴涵所需时间与数据库成线性关系 最重要的是最后一个性质第3章 逻辑系统58 简要介绍2种推理算法简单的前向链接算法和简单的后向链接算法,结合一个例子说明算法的应用 一阶推理规则一般化分离规则(Generalized Modus Ponens) 对于原子语句pi, pi, q, 存在置换,使得(pi)= (pi), 对所有i都成立, 则第3章 逻辑系统)().( , .11qqppppnn59 置换(或代换):设x1xn是n个变量,且各不相同,t1tn是n个项(常量、变量、函数)
29、,tixi,则有限序列t1/x1, t2/x2 tn/xn称为一个置换 置换乘积(合成):设和是2个置换,则先后作用于公式或项,称为置换乘积,用表示。 通过相关的置换,使不同的一阶公式成为一样的,这个过程称为合一第3章 逻辑系统60 合一置换:设有一组谓词公式E1Ek和置换,使E1=E2=Ek,则称为合一置换,E1Ek称为可合一的 / 合一置换也叫通代 最一般合一置换(最广通代):如果和都是公式组E1Ek的合一置换,且有置换存在,使得=,则称为公式组E1Ek的最一般合一置换,记为mgu (most general unification)第3章 逻辑系统61 有子句 x King(x) Gre
30、edy(x) Evil(x) King(John) Greedy(John) 则做置换 =x/John, 用一般化分离规则可得: q=Evil(John)第3章 逻辑系统62 对于合一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章介绍第3章 逻辑系统63 问题描述: 美国法律规定:
31、美国人(American)卖武器(weapon)给敌对国家(hostile)是犯罪的(criminal). 美国的敌国Nono有一些导弹(missile),所有这些导弹是West上校卖给他们的,而West上校是一个美国人 证明:West是犯罪的第3章 逻辑系统64 用确定子句表示上述内容 美国人卖武器给敌对国家是犯罪的American(x) Weapon(y) Sell(x,y,z) Hostile(z) Criminal(x)1 Nono有一些导弹x Own(Nono, x) Missile(x) 消去其中的存在量词,引入新常量,得到2个原子公式(正文字)Own(Nono, M1) 4Mis
32、sile(M1) 5第3章 逻辑系统65 所有该国导弹都是West上校出售的Missile(y) Own(Nono, y)Sell(West, y, Nono) 2 导弹是武器Missile(y) Weapon(y)3 其它陈述:美国人West American(West)6敌国 Nono Hostile(Nono)7 上述描述放入知识库:13为确定子句(上述原始形式均可以化为原子的析取且只有一个正文字), 47为正文字第3章 逻辑系统66 前向链接算法的推理过程: 从已知事实(知识库中的原子公式)开始,依次对知识库中的规则(以确定子句的形式出现)进行置换,检查规则前提部分的文字是否全部与知识
33、库中的事实相匹配 如果是匹配的,则把该条规则已经做过置换的结论部分添加到知识库中,如果这个结论和查询(既需要推导出的结论)一致,则推理结束,获得证明第3章 逻辑系统67 重复上述过程,直到获得证明;或者再没有新的事实(推出的结论)加入,则此时推理以证明失败结束 约束:要求每次加入知识库的结论都是全新的,而不是已知事实的重命名(即谓词相同只是变量名不同)第3章 逻辑系统68Function FC(KB,) Return a substitution or FALSEInputs: KB , a set of first-order definite clauses / , the query =
34、 an atomlocal variables : new, the new rules inferred on each iterationrepeat until new is empty newfor each rule r (in the form of define clause) in KB do for each such that (p1pn)= (p1pn)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
35、 new to KBreturn false 第3章 逻辑系统69第3章 逻辑系统 使用前向链接算法对前面的例子进行推理 用知识库中的事实(即47)依次对知识库中的各个子句进行置换操作并用推理规则获得新的文字 第一次循环体执行: 子句1前提部分未获满足(为什么?) 子句2使用置换x/M1, 则可得Sell(West, M1, Nono)8 子句3使用置换x/M1,则可得Weapon(M1)970第3章 逻辑系统 此时new中为89,为原知识库所未有,将它们添加到知识库中 第二次循环体执行: 再次循环时new首先清空 子句1置换x/West, y/M1, z/Nono得到Criminal(Wes
36、t)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 原始查询(既要证明的结论)以目标列表的形式出现,开始时列表中只有一个元素 列表的操作相当于栈,是一个递归过程(如下)即深度优先的搜索过程 推理过程是从结论(子句的头)开始,找到匹配的头就扩展这个头所在的规则体;扩展部分又作为头继续扩展,直到全部原子均与事实相匹配 比较:正向=事
37、实结论/反向=结论事实第3章 逻辑系统73 算法的推理过程是: 选取栈当中的第一个目标,在知识库中寻找子句的头(即结论部分)能与目标合一的每个子句 每个这样的子句创建了一个递归调用过程,在这个递归调用过程中子句的前提(子句的体)被加入到目标栈当中 当栈中所有目标都得到匹配,则当前的证明分支是成功的 注意:事实是指有头没有体的子句(正文字)第3章 逻辑系统74 在算法中answers作为存放置换的数据结构,返回一系列置换操作,这些操作说明了反向链接算法获取证明的过程 在算法中包括了置换的合成(或者写为Compose(,),其效果就是依次进行每个置换第3章 逻辑系统75 第一次应用算法,对于待证明
38、的目标来说,本身就是一个正文字,此时要用这个文字中的常量对合适的规则(子句的头与该文字匹配)进行置换 这个置换通过递归调用带入下一次置换,就得到了合成置换 在本例中有:初始x/West 递归x/West, y/M1递归x/West, y/M1, z/Nono第3章 逻辑系统76Function BC(KB, goals, ) returns a set of substitutionsInputs: KB, goals=a list of conjuncts forming a query ( already applied), =the current substitution (initi
39、al=)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, )answersreturn answers第3章 逻辑系统77 反向链接算法推理过程
40、 目标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第3章 逻辑系统78 再次递归调用Sell(West, M1, z)得到置换=z/Nono,递归返回复合置换x/West
41、, y/ M1, z/Nono 在置换过程中每个变量只能置换一个常量作为约束,减少置换的不定性 此时子目标全部匹配,再无新的子目标生成,返回置换集合结束第3章 逻辑系统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/Nonoy/M180 前向链接算法特点:数据驱动 / 是可靠的和完备的 后向链接算法特点:目标驱动 / 是可靠的但不是完备的(书中p220/p224) 可以从“是否能找到
42、问题的解”角度考虑不完备性 后向链接算法根据目标来进行相关事实的匹配,对于大规模的知识库来说有助于减小搜索空间第3章 逻辑系统81 Stuart Russell / Peter Norvig: AIMA 第7章 /第8章 /第9章 陆汝钤 编著: 人工智能(上册) 第1章 陆钟万,面向计算机科学的数理逻辑,科学出版社,1998年1月第1版 朱梧木贾、肖奚安,数理逻辑引论,南京大学出版社,1995年5月第1版 王元元,计算机科学中的逻辑学,科学出版社,1989年9月第1版第3章 逻辑系统附录 形式系统简介F1 形式系统和形式推演F2 形式系统的语义F3 形式系统的整体特征第3章 逻辑系统F1 形
43、式系统定义和形式推演第3章 逻辑系统84 逻辑的形式系统的定义 一个形式系统Formal System由5个部分组成:(1)符号表,非空集合,即形式语言(如Lp和L);(2)上全体符号的集合*的一个子集TERM,其 元 素 称 为 F S 的 项 ; T E R M 有 子 集VARIABLE,其元素称为变量;(3)*的一个子集FORMULA,其元素称为FS的公式;FORMULA有子集ATOM,其元素称为原子公式;TERMFORMULA=;第3章 逻辑系统85(4)FORMULA的一个子集AXIOM,其元素称为FS的公理;(5)FORMULA上的n元关系集合RULE,其元素称为FS的推理规则。
44、 其中、TERM、FORMULA称为FS的组成部分,AXIOM、RULE称为FS的推演部分 公理推演系统包括AXIOM,而自然推演系统只包括推理规则第3章 逻辑系统86 对象语言和元语言:作为被研究对象的语言称为对象语言,用以研究对象语言的语言称为元语言 例子:用汉语研究英语语法,则英语是对象语言,汉语是元语言 数理逻辑中的形式系统各有其自身的形式语言如Lp和L,这些是被研究的对象,因而是对象语言;但为了研究这些形式系统,又必须使用某种语言,那么这种语言便是元语言第3章 逻辑系统87 如:“鸟正在飞翔”描述对象语言;“命题鸟正在飞翔真”对上句的评论元语言。 形式系统的对象语言,其中的符号既是对
45、客观对象的抽象,用于研究客观对象;同时又是一种符号客体,是被研究的对象第3章 逻辑系统88 形式系统的元语言包括: 对形式系统中组成成分的称谓项、公式、公理等 逻辑术语如果-那么、当且仅当、存在、所有等 对形式系统性质(整体特征)的描述如一致性、完备性、可判定性等,该部分最重要 元语言中使用的符号:自然语言(如汉语)和一些被引进的符号,如:、|= 等 未经解释的形式语言可以没有含义,但元语言必须有其具体含义。第3章 逻辑系统89 元理论是关于形式系统的理论,包括三部分内容: 关于形式系统语法(syntax)的研究,不涉及具体意义的符号体系,研究符号串的推演,即形式推演; 关于形式系统语义(se
46、mantics)的研究,研究形式系统在被作出各种解释时的性质; 关于形式系统语法和语义关系的研究,特别是形式系统的性质,如:合理性、完备性等。第3章 逻辑系统90 形式推演:定义了公式之间的形式可推演性关系,它涉及公式的语法结构,其正确性能够机械地证明 用记号 表示形式可推演关系,读作“推出” 用 A表示A是由形式可推演的(或形式可证明的),其中是前提,A是结论 记号不是形式语言中的符号, A也不是形式语言中的公式,而是元语言中的命题第3章 逻辑系统91 形式推演由形式推演的规则定义 命题逻辑中有一些常用的推演规则(规则模式) 肯定前提if A then A () 增加前提if A then
47、, A (+) 自反A A (Ref) 传递if A then A ()第3章 逻辑系统92 消去(反证律)if , A B & , AB then A(-) 引入(归谬律) if , A B & , A B then A(+) 消去if AB, Athen B(-) 引入if , A B then AB(+)第3章 逻辑系统93 消去if AB then A, B(-) 引入if A, B then AB(+) 消去if , A C & ,B C then ,AB C (-) 引入if A then AB, BA(+)第3章 逻辑系统94 消去if AB, A then Bif AB, B
48、then A() 引入if , A B & , B A then AB (+) 通过连接词的增减或变形,实现公式的变换 常用AB AB第3章 逻辑系统95 (命题逻辑)形式可推演性:在命题逻辑中,A是由可形式推演的(或形式可证明的),记为A,当且仅当A能通过有限次应用命题逻辑的形式推演规则生成 即A成立,当且仅当存在有限序列使得 1A1,2A2,nAn 中的每一项均由某个形式推导规则生成,且nAn 就是A即n=,An=A第3章 逻辑系统96 用 A表示A不成立 用A|-|B表示左右两边的公式可以互相推出,称其为语法等值公式或等值公式 建立在上述形式推演规则基础上的形式推演系统称为自然推演(演绎
49、)系统第3章 逻辑系统97 命题逻辑中的形式推演规则都包括在一阶逻辑当中,但是其中出现的公式是一阶语言中的公式,另外增加了关于量词的规则 (一阶逻辑)形式可推演性:在一阶逻辑中,A是由可形式推演的(或形式可证明的),记为A,当且仅当A能通过有限次应用一阶逻辑的形式推演规则生成 形式推演的例子可以参考本章后面列出的3本关于逻辑的教科书第3章 逻辑系统F2 形式系统的语义第3章 逻辑系统99 语义即对形式语言进行解释 研究可推导性即形式推演()时不考虑作为前提和结论的命题的内容,只考虑命题真假并由此确定前提的真是否蕴涵结论的真,即前提和结论之间是否有可推导关系(语法) 研究形式系统的语义时,对形式
50、系统赋予研究对象的集合即论域;用论域中的个体对象、对象之上的运算(函数)、对象之间的关系(谓词)去解释形式系统中的符号,称作指称denote 指称语义学第3章 逻辑系统100 赋予形式系统的论域及解释称为形式系统的语义结构,简称结构(structure)/ 结构及其在该结构下公式所取真值的规定,称为形式系统的指称语义(denotational semantics)第3章 逻辑系统101 研究命题逻辑的语义,即研究公式(公式集)的真假赋值问题 真假赋值:真假赋值是以所有命题符号的集合为定义域,以真假值1,0为值域的函数。真假赋值v给公式A指派的值记作Av 可满足性:是可满足的,当且仅当有真假赋值