《人工智能自动推理33723.pptx》由会员分享，可在线阅读，更多相关《人工智能自动推理33723.pptx（212页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。
1、2023/5/111第第4章章自动推理自动推理2023/5/1124.1 引 言2023/5/113什么是推理什么是推理p推理就是推理就是按某种策略由已知判断推出另一判断按某种策略由已知判断推出另一判断的思维过程的思维过程p已知判断：包括已掌握的与求解问题有关的知已知判断：包括已掌握的与求解问题有关的知识及关于问题的已知事实识及关于问题的已知事实 推理的结论：由已知判断推出新判断推理的结论：由已知判断推出新判断p推理由程序程序实现，称为推理由程序程序实现，称为推理机推理机2023/5/114推理方式及其分类推理方式及其分类 1 1、演绎推理、归纳推理、默认推理、演绎推理、归纳推理、默认推理p推
2、理的基本任务是推理的基本任务是从一种判断推出另一种判断从一种判断推出另一种判断p按判断按判断推出的途径推出的途径来划分，可分为演绎推理、归纳推理及默来划分，可分为演绎推理、归纳推理及默认推理认推理（1 1）演绎推理）演绎推理演绎推理是从演绎推理是从全称判断全称判断推导出推导出特称判断特称判断或或单称判断单称判断的过程的过程演绎推理有多种形式，经常用的是三段论式演绎推理有多种形式，经常用的是三段论式三段论式包括三段论式包括大前提：已知的一般性知识或假设大前提：已知的一般性知识或假设小前提：关于所研究的具体情况或个别事实的判断小前提：关于所研究的具体情况或个别事实的判断结论：由大前提推出的适合于小
3、前提所示情况的新判结论：由大前提推出的适合于小前提所示情况的新判断断2023/5/115推理方式及其分类推理方式及其分类n在任何情况下，由演绎推导出的结论都是蕴涵在大前提在任何情况下，由演绎推导出的结论都是蕴涵在大前提的一般性知识中的一般性知识中n只要大前提和小前提是正确的，则由它们推出的结论必只要大前提和小前提是正确的，则由它们推出的结论必然是正确的然是正确的(2)(2)归纳推理归纳推理n归纳推理是从足够多的事例中归纳出一般性结论的推理归纳推理是从足够多的事例中归纳出一般性结论的推理过程，是一种过程，是一种从个别到一般从个别到一般的推理的推理n归纳推理：归纳推理：完全归纳推理完全归纳推理、不
4、完全归纳推理不完全归纳推理n完全归纳推理是在进行归纳时考察了相应事物的全部对完全归纳推理是在进行归纳时考察了相应事物的全部对象，并根据这些对象是否都具有某种属性，从而推出这象，并根据这些对象是否都具有某种属性，从而推出这个事物是否具有这个属性个事物是否具有这个属性n不完全归纳推理是指只考察了相应事物的部分对象就得不完全归纳推理是指只考察了相应事物的部分对象就得出了结论出了结论2023/5/116推理方式及其分类推理方式及其分类n枚举归纳推理：若已知某类事物的有限可数个具体事枚举归纳推理：若已知某类事物的有限可数个具体事物都具有某种属性，则可推出该类事物都具有此属性物都具有某种属性，则可推出该类
5、事物都具有此属性n类比推理：在两个或两类事物有许多属性都相同或相类比推理：在两个或两类事物有许多属性都相同或相似的基础上，推出它们在其他属性上也相同或相似的似的基础上，推出它们在其他属性上也相同或相似的一种推理一种推理(3)(3)默认推理默认推理n又称缺省推理，它是在知识不完全的情况下假设某些条又称缺省推理，它是在知识不完全的情况下假设某些条件已经具备所进行的推理件已经具备所进行的推理n摆脱了需要知道全部事实才能进行推理的需求，使得在摆脱了需要知道全部事实才能进行推理的需求，使得在知识不完全的情况下也能进行推理知识不完全的情况下也能进行推理2023/5/117推理方式及其分类推理方式及其分类2
6、 2、确定性推理、不确定性推理、确定性推理、不确定性推理p按推理时所用知识的确定性来划分，推理可分为按推理时所用知识的确定性来划分，推理可分为确定性推理、不确定性推理确定性推理、不确定性推理p确定性推理（精确推理）：确定性推理（精确推理）：推理时所用的知识都推理时所用的知识都是精确的，推出的结论也是确定的，其真值或者是精确的，推出的结论也是确定的，其真值或者为真，或为假，没有第三种情况出现为真，或为假，没有第三种情况出现p不确定性推理（不精确推理）：不确定性推理（不精确推理）：推理时所用的知推理时所用的知识不都是精确的，推出的结论也不完全是肯定的，识不都是精确的，推出的结论也不完全是肯定的，真
7、值位于真与假之间，命题的外延模糊不清真值位于真与假之间，命题的外延模糊不清2023/5/118推理方式及其分类推理方式及其分类3 3、单调推理、非单调推理、单调推理、非单调推理p按推理过程中推出的结论是否单调地增加，或推出按推理过程中推出的结论是否单调地增加，或推出的结论是否越来越接近目标，可分为单调推理和非的结论是否越来越接近目标，可分为单调推理和非单调推理单调推理p单调推理：单调推理：在推理过程中随着推理的向前及新知识在推理过程中随着推理的向前及新知识的加入，推出的结论是呈单调增加的趋势，并且越的加入，推出的结论是呈单调增加的趋势，并且越来越接近最终目标，在推理过程中不出现反复的情来越接近
8、最终目标，在推理过程中不出现反复的情况况p非单调推理：非单调推理：在推理过程中由于新知识的加入，不在推理过程中由于新知识的加入，不仅没有加强已推出的结论，反而要否定它，使得推仅没有加强已推出的结论，反而要否定它，使得推理退回到前面的某一步，重新开始理退回到前面的某一步，重新开始 非单调推理往往在信息不完全或者情况发生变化非单调推理往往在信息不完全或者情况发生变化时时出现。出现。2023/5/119推理的控制策略推理的控制策略p推理过程是一个思维过程，即推理过程是一个思维过程，即求解问题的过程求解问题的过程p推理的控制策略主要包括推理方向、搜索策略、推理的控制策略主要包括推理方向、搜索策略、冲突
9、消解策略、求解策略及限制策略等冲突消解策略、求解策略及限制策略等1 1、推理方向、推理方向n推理方向用于确定推理的驱动方式，分为正向推理方向用于确定推理的驱动方式，分为正向推理、逆向推理、混合推理及双向推理四种推理、逆向推理、混合推理及双向推理四种知识库综合数据库推理机2023/5/1110推理的控制策略推理的控制策略正向推理正向推理 正向推理是从初始状态出发，使用规则，正向推理是从初始状态出发，使用规则，到达目标状态。又称为数据驱动推理、前向到达目标状态。又称为数据驱动推理、前向链推理、模式制导推理及前件推理。链推理、模式制导推理及前件推理。逆向推理逆向推理 逆向推理是以某个假设目标为出发点
10、的逆向推理是以某个假设目标为出发点的一种推理，又称为目标驱动推理、逆向链推一种推理，又称为目标驱动推理、逆向链推理、目标制导推理及后件推理理、目标制导推理及后件推理2023/5/1111正、逆向推理比较正、逆向推理比较项项目目正向推理正向推理逆向推理逆向推理驱动方式驱动方式数据驱动数据驱动目标驱动目标驱动推理方法推理方法从一组数据出发向前推导结论从一组数据出发向前推导结论从可能的解出发向后推理验证解答从可能的解出发向后推理验证解答启动方法启动方法从一个事件启动从一个事件启动由询问关于目标状态的一个问题启动由询问关于目标状态的一个问题启动透明程度透明程度不能解释其推理过程不能解释其推理过程可解释
11、其推理过程可解释其推理过程推理方向推理方向由底向上推理由底向上推理由顶向下推理由顶向下推理典型系统典型系统CLIPSCLIPS，OPSOPSPROLOGPROLOG2023/5/1112推理的控制策略推理的控制策略混合推理混合推理p已知的事实不充分。通过正向推理先把其运用条件不能已知的事实不充分。通过正向推理先把其运用条件不能完全匹配的知识都找出来，并把这些知识可导出的结论完全匹配的知识都找出来，并把这些知识可导出的结论作为假设，然后分别对这些假设进行逆向推理作为假设，然后分别对这些假设进行逆向推理p由正向推理推出的结论可信度不高由正向推理推出的结论可信度不高p希望得到更多的结论希望得到更多的
12、结论p推理的形式：推理的形式：n先正向再逆向先正向再逆向，通过正向推理，即从已知事实演绎出，通过正向推理，即从已知事实演绎出部分结果，然后再用逆向推理证实该目标或提高部分结果，然后再用逆向推理证实该目标或提高 其其可信度可信度n先逆向再正向先逆向再正向，先假设一个目标进行逆向推理，然后，先假设一个目标进行逆向推理，然后再利用逆向推理中得到的信息进行正向推理，以推出再利用逆向推理中得到的信息进行正向推理，以推出更多的结论更多的结论2023/5/1113推理的控制策略推理的控制策略双向推理双向推理双向推理是指正向推理与逆向推理同时进行，双向推理是指正向推理与逆向推理同时进行，且在推理过程中的某一步
13、骤上且在推理过程中的某一步骤上“碰头碰头”的一的一种推理。种推理。正向推理所得的中间结论恰好是逆向推理此正向推理所得的中间结论恰好是逆向推理此时要求的证据时要求的证据2 2、求解策略、求解策略 推理是只求一个解还是求所有解以及最优解等推理是只求一个解还是求所有解以及最优解等3 3、限制策略、限制策略 对推理的深度、宽度、时间、空间等进行限制对推理的深度、宽度、时间、空间等进行限制2023/5/1114推理的控制策略推理的控制策略4 4、冲突消解策略 p在推理过程中，匹配会出现三种情况在推理过程中，匹配会出现三种情况n已知事实不能与知识库中的任何知识匹配成功已知事实不能与知识库中的任何知识匹配成
14、功n已知事实恰好只与知识库中的一个知识匹配成功已知事实恰好只与知识库中的一个知识匹配成功n已知事实可与知识库中的多个知识匹配成功；或者有多已知事实可与知识库中的多个知识匹配成功；或者有多个（组）已知事实都可与知识库中某一知识匹配成功；个（组）已知事实都可与知识库中某一知识匹配成功；或者有多个（组）已知事实可与知识库中的多个知识匹或者有多个（组）已知事实可与知识库中的多个知识匹配成功配成功出现冲突的情况出现冲突的情况对正向推理而言，如果有多条产生式规则的前件都和已对正向推理而言，如果有多条产生式规则的前件都和已知的事实匹配成功；或者有多组不同的已知事实都与同知的事实匹配成功；或者有多组不同的已知
15、事实都与同一条产生式规则的前件匹配成功；或者两种情况同时出一条产生式规则的前件匹配成功；或者两种情况同时出现现2023/5/1115推理的控制策略推理的控制策略对逆向推理而言，如果有多条产生式的后件都和同一假设匹配成功，或者有多条产生式后件可与多个假设匹配成功。按就近原则排序l该策略把最近被使用过的规则赋予较高的优先级。按已知事实的新鲜性排序 l一般我们认为新鲜事实是对旧知识的更新和改进，比老知识更有效，即后生成的事实比先生成的事实具有较大的优先性。2023/5/1116推理的控制策略推理的控制策略按匹配度排序 l在不确定推理时，匹配度不仅可确定两个知识模式是否可匹配，还可用于冲突消解。根据匹
16、配程度来决定哪一个产生式规则优先被应用。按领域问题特点排序 l该方法按照求解问题领域的特点将知识排成固定的次序。按上下文限制排序l该策略将知识按照所描述的上下文分成若干组，在推理过程中根据当前数据库中的已知事实与上下文的匹配情况，确定选择某组中的某条知识。2023/5/1117推理的控制策略推理的控制策略按条件个数排序l多条规则生成的结论相同的情况下，由于条件个数较少的规则匹配所花费的时间较少而且容易实现，所以将条件少的规则赋予较高的优先级，优先被启用。按规则的次序排序 l该策略是以知识库中预先存入规则的排列顺序作为知识排序的依据，排在前面的规则具有较高的优先级。2023/5/11184.3
17、自然演绎推理2023/5/1119自然演绎推理的基本概念p定义：自然演绎推理是指从一组已知的事实出发，直接运用命题逻辑或谓词逻辑中的推理规则推出结论的过程。p推理规则：nP规则：在推理的任何步骤上都可引入前提，继续进行推在推理的任何步骤上都可引入前提，继续进行推理。理。nT规则：推理时，如果前面步骤中有一个或多个公式永真推理时，如果前面步骤中有一个或多个公式永真蕴涵公式蕴涵公式S S，则可把，则可把S S引入推理过程中。引入推理过程中。n反证法：，当且仅当，当且仅当 。即：。即：Q Q为为P P的逻辑的逻辑结论，当且仅当结论，当且仅当 是不可满足的。是不可满足的。2023/5/1120自然演绎
18、推理的基本概念p假言推理 表示：由表示：由 及及P P为真，可推出为真，可推出Q Q为真为真 p拒取式推理 表示：由表示：由 为真及为真及Q Q为假，可推出为假，可推出P P为假为假 2023/5/1121自然演绎推理的基本概念自然演绎推理的基本概念n肯定后件肯定后件(Q)(Q)的错误：当的错误：当PQPQ为真时为真时,希望通过肯希望通过肯定后件定后件Q Q推出前件推出前件P P为真为真,这是不允许的这是不允许的.n否定前件否定前件(P)(P)的错误：当的错误：当PQPQ为真时为真时,希望通过否希望通过否定前件定前件P P推出后件推出后件Q Q为假为假,这也是不允许的这也是不允许的.n避免产生
19、两类错误：避免产生两类错误：2023/5/1122自然演绎推理的基本概念自然演绎推理的基本概念n如果行星系统是以太阳为中心的如果行星系统是以太阳为中心的,则金星会显示出则金星会显示出位相变化。位相变化。n金星会显示出位相变化。金星会显示出位相变化。n所以，行星系统是以太阳为中心的。所以，行星系统是以太阳为中心的。n如伽利略在论证哥白尼的日心说时如伽利略在论证哥白尼的日心说时,曾使用曾使用了下列推理：了下列推理：这就是使用了肯定后件的推理，违反了经典逻辑的逻辑规则,他为此曾遭到非难。2023/5/1123自然演绎推理的基本概念自然演绎推理的基本概念n如果上网，则能知道新闻。如果上网，则能知道新闻
20、。n没有上网。没有上网。n所以，不知道新闻。所以，不知道新闻。n又如下列推理：又如下列推理：这就是使用了否定前件的推理,违反了逻辑规则,显然是不正确的,因为通过收听广播、看电视等，也会知道新闻。2023/5/1124自然演绎推理的优缺点自然演绎推理的优缺点n优点：优点：定理证明过程自然，容易理解，而且它拥有丰富的定理证明过程自然，容易理解，而且它拥有丰富的推理规则，推理过程灵活，便于在它的推理规则中推理规则，推理过程灵活，便于在它的推理规则中嵌入领域启发式知识。嵌入领域启发式知识。n缺点：缺点：容易产生组合爆炸，推理过程中得到的中间结论容易产生组合爆炸，推理过程中得到的中间结论一般呈指数形式递
21、增。一般呈指数形式递增。2023/5/1125 人的问题求解行为更像是一个人的问题求解行为更像是一个解答识别解答识别过程而非过程而非解答搜索解答搜索过程过程 识别解答或部分解答依赖于应用领域特有的知识，识别解答或部分解答依赖于应用领域特有的知识，符号推理则成为基于知识来求解问题的主要手段。符号推理则成为基于知识来求解问题的主要手段。符号推理的重要方式是演绎推理符号推理的重要方式是演绎推理 它的基础为谓词演算它的基础为谓词演算一种一种形式语言形式语言 将各种陈述性（说明性）的描述以将各种陈述性（说明性）的描述以形式化形式化的方式表示，以的方式表示，以便对它们便对它们 作处理。作处理。谓词演算谓词
22、演算人工智能系统最常用的知识表示方法，人工智能系统最常用的知识表示方法，广泛地应用于各种人工智能系统的设计。广泛地应用于各种人工智能系统的设计。谓谓词词演演算算（或或更更广广义义地地，形形式式逻逻辑辑）是是人人工工智智能能研研究究的的重重要要基基础础之一。之一。主要内容：主要内容：谓词演算谓词演算 H H域和海伯伦定理域和海伯伦定理 归结原理归结原理 归结反演归结反演 归结归结演演绎绎推理推理 2023/5/1126回顾谓词逻辑表示法回顾谓词逻辑表示法p1、谓词公式、谓词公式n“谓词公式谓词公式”的一般形式：的一般形式：pP(x1,x2,xn)，其中，其中，pP谓词符号谓词符号（简称谓词）；（
23、简称谓词）；pXi(i=1,2,n)参数项参数项（简称项），项可以（简称项），项可以是常量是常量、变变量量或或函数函数；pP(x1,x2,xn)n元谓词公式；元谓词公式；n“谓词公式谓词公式”的基本组成：的基本组成：p谓词符号谓词符号、常量符号常量符号、变量符号变量符号、函数符号函数符号；p用用括号括号和和逗号逗号隔开，隔开，表示论域内的关系表示论域内的关系。n“谓词公式谓词公式是谓词逻辑的基本单元，也称为是谓词逻辑的基本单元，也称为原子公式原子公式。2023/5/1127p2、连词和量词、连词和量词n通过引入通过引入连词连词和和量词量词，可以把，可以把谓词公式（原子公式）谓词公式（原子公式）
24、组合为组合为复合谓词公复合谓词公式式。n复合谓词公式复合谓词公式也称为也称为逻辑语句逻辑语句。p（1）连词）连词（非）加在（非）加在谓词公式谓词公式前面，称为否定，或取反。前面，称为否定，或取反。（与）连接（与）连接谓词公式谓词公式，称为，称为合取合取；产生的产生的逻辑语句逻辑语句称为称为合取式合取式，每个成分成为，每个成分成为合取项。合取项。（或）连接（或）连接谓词公式谓词公式，称为，称为析取析取；产生的产生的逻辑语句逻辑语句称为称为析取式析取式，每个成分成为，每个成分成为析取项。析取项。（蕴涵）连接（蕴涵）连接谓词公式谓词公式产生产生蕴涵式蕴涵式；左部称为左部称为前项前项，右部称为，右部称
25、为后项后项。（等价）连接（等价）连接谓词公式谓词公式产生产生等价式等价式；正、逆向蕴涵式的合取。；正、逆向蕴涵式的合取。2023/5/1128p2、连词和量词、连词和量词n通过引入连词和量词，可以把通过引入连词和量词，可以把原子公式原子公式组合为组合为复合谓词公式复合谓词公式。n复合谓词公式也称为复合谓词公式也称为逻辑语句逻辑语句。p（1）连词）连词n通过连词产生的复合谓词公式（逻辑语句）的通过连词产生的复合谓词公式（逻辑语句）的真值表真值表：PQ PPQPQP QP QTTFTTTTFTTFTTFTFFFTFFFFTFFTT2023/5/1129p2、连词和量词、连词和量词n命题命题不包含不
26、包含变量变量的的谓词公式谓词公式和和逻辑语句逻辑语句；n命命题题逻逻辑辑基基于于命命题题的的谓谓词词逻逻辑辑称称为为命命题题逻逻辑辑，命命题逻辑是谓词逻辑的子集题逻辑是谓词逻辑的子集。n命题逻辑命题逻辑缺乏有效的表达缺乏有效的表达一般性概念一般性概念的能力的能力p无法把每个知识单元抽象、细分；无法把每个知识单元抽象、细分；p如，如，“条条大路通罗马条条大路通罗马”。pLead(Road1,Roma)pLead(Road2,Roma)n谓词逻辑谓词逻辑中引入中引入变量变量和对变量进行约束的和对变量进行约束的量词量词。p（2）量词）量词n全称量词全称量词 存在量词存在量词 2023/5/1130p
27、2、连词和量词、连词和量词（2）量词）量词n全称量词全称量词 p符号符号(x)P(x)：表示对于某个论域中的：表示对于某个论域中的所有（任意一个）所有（任意一个）个体个体x,都有都有P(x)真值为真值为T。n存在量词存在量词 p符号符号(x)P(x)：来表示某个论域中：来表示某个论域中至少存在一个至少存在一个个体个体x，使，使P(x)真值为真值为T。条条大路通罗马条条大路通罗马Mary给每个人一本书给每个人一本书Mary给每人某个同样的东西给每人某个同样的东西量词可以嵌套使用量词可以嵌套使用可以有不受量词约束的变量可以有不受量词约束的变量2023/5/1131p2、连词和量词、连词和量词（2）
28、量词）量词n全称量词全称量词 p符号符号(x)P(x)：表示对于某个论域中的：表示对于某个论域中的所有（任意一个）所有（任意一个）个体个体x,都有都有P(x)真值为真值为T。n存在量词存在量词 p符号符号(x)P(x)：来表示某个论域中：来表示某个论域中至少存在一个至少存在一个个体个体x，使，使P(x)真值为真值为T。条条大路通罗马条条大路通罗马所有机器人都是灰色的所有机器人都是灰色的2023/5/1132p一阶谓词逻辑一阶谓词逻辑n定义：定义：若限定若限定不允许不允许对对谓词谓词和和函数名函数名进行进行量化量化处处理，且理，且参数项参数项不能是不能是谓词公式谓词公式，则这样的谓词逻，则这样的
29、谓词逻辑是辑是一阶一阶的。的。p谓词、函数名谓词、函数名的出现位置的出现位置不允许使用变量不允许使用变量；p参数项参数项不能是不能是谓词公式谓词公式；n(P)P(A)-谓词进行了量化；谓词进行了量化；n(y)Married(y(L1),Mary)-函数名进行了量化；函数名进行了量化；nP(x,Q(y)-参数项是谓词公式；参数项是谓词公式；2023/5/1133合适合适(式式)公式公式p1、合适公式的定义、合适公式的定义n合适公式合适公式适合于适合于一阶谓词逻辑一阶谓词逻辑n遵从以下递归方式定义的遵从以下递归方式定义的逻辑语句逻辑语句称为称为合适公式合适公式n单一谓词公式是合适公式；单一谓词公式
30、是合适公式；n若若A A是合适公式，则是合适公式，则 A A也是合适公式；也是合适公式；n若若A A和和B B都是合适公式，则都是合适公式，则A AB B、A AB B、A AB B和和A AB B也都也都是合适公式；是合适公式；n若若A A是合适公式，是合适公式，x x是约束变量，则是约束变量，则(x x)A)A和和(x x)A)A也都是也都是合适公式；合适公式；n只有按上述规则只有按上述规则-求得的公式，才是合适公式。求得的公式，才是合适公式。n连词优先级别连词优先级别是是，、，、，但可通过，但可通过括号括号改变优改变优先级。先级。2023/5/1134合适公式的性质合适公式的性质合适公式
31、等价关系合适公式等价关系:1.1.否定之否定否定之否定 (P)P)P P 2.2.蕴涵式转化蕴涵式转化 P PQ Q PQPQ 3.3.狄摩根定律狄摩根定律 (PQ)(PQ)PPQQ (PQ)(PQ)PPQQ4.4.分配律分配律5.5.P(QR)P(QR)(PQ)(PR(PQ)(PR）P(QR)P(QR)(PQ)(PR)(PQ)(PR)6.6.5.5.交换律交换律 PQ PQ QP QPP P QQ QP QP 2023/5/1135合适公式的性质合适公式的性质6.6.结合律结合律 (PQ)R(PQ)R P(QR P(QR）(PQ)R(PQ)R P P（QRQR）7.7.逆否律逆否律 P PQ
32、 Q Q Q P P 8.8.量词否定量词否定 (x)P(x)x)P(x)(x)(x)(P(x)P(x)(x)P(x)x)P(x)（x)(x)(P(x)P(x)2023/5/1136合适公式的性质合适公式的性质9.9.量词分配量词分配 (x)P(x)Q(x)x)P(x)Q(x)(x)P(x)(x)P(x)(x)Q(x)x)Q(x)(x x）P(x)Q(x)P(x)Q(x)（x x）P(x)(P(x)(x)Q(x)x)Q(x)10.10.约束变量的虚元性约束变量的虚元性(x)P(x)x)P(x)(y)P(y)y)P(y)(x)P(x)x)P(x)(y)P(y)y)P(y)(x)x)P(x)Q(x
33、)P(x)Q(x)(x)x)P(x)(P(x)(y y)Q(Q(y y)(x)x)P(x)Q(x)P(x)Q(x)(x)x)P(x)(P(x)(y y)Q(Q(y y)2023/5/1137合适公式的标准化合适公式的标准化p1、标准化需求、标准化需求n常见的基于谓词演算的推理：常见的基于谓词演算的推理：归结反演归结反演、(正向正向/逆向逆向)归结演绎推理归结演绎推理p要求以要求以量词前束范式量词前束范式来表示合适公式来表示合适公式n量词前束范式量词前束范式形式如下：形式如下：p(Q1x1)(Q2x2)(Qkxk)M，其中，其中pM母式，不包括任何量词；母式，不包括任何量词；pQixiQi可以是
34、可以是量词量词符号符号 或或；xi是量词的是量词的约束变量约束变量(i=1,2,k)2023/5/1138前束范式前束范式例1：变公式（：变公式（x）P（x）=（x）Q（x）为）为前束范式前束范式（x）P（x）（x）Q（x）（x）（）（P（x）（x）Q（x）（x）（）（P（x）Q（x）为前束范式）为前束范式2023/5/1139前束范式前束范式例例2：(x)(y)(z)(P(x，z)P(y，z)=(u)Q(x，y，u)x)(y)(z)(P(x，z)P(y，z)(u)Q(x，y，u)(x)(y)(z)(P(x，z)P(y，z)(u)Q(x，y，u)x)(y)(z)(u)(P(x，z)P(y，z)
35、Q(x，y，u)2023/5/1140史柯伦标准型及其构造思想史柯伦标准型及其构造思想p史柯伦（Skolem）标准型：海伯伦：海伯伦（Herbrand）定理是归结原理的基础。海伯伦定）定理是归结原理的基础。海伯伦定理证明的步骤实际上是反演法，即不是证明一个理证明的步骤实际上是反演法，即不是证明一个公式是永真，而是证明该公式是否是公式是永真，而是证明该公式是否是永假永假的。反的。反演法利用了一个标准型，这个标准型就是演法利用了一个标准型，这个标准型就是Skolem标准型。标准型。2023/5/1141一阶逻辑公式所对应的一阶逻辑公式所对应的Skolem标标准型基于如下思想来构造：准型基于如下思想
36、来构造：1.一阶逻辑的一个公式被变换为前束范式。其中前束是一个一阶逻辑的一个公式被变换为前束范式。其中前束是一个存在量词存在量词或或全称量词全称量词的序列，母式中不在含有量词。的序列，母式中不在含有量词。2.因为母式不含量词，所以可以变换为因为母式不含量词，所以可以变换为合取合取范式。范式。3.通过使用通过使用Skolem函数，可以在前束中将存在量词消去，函数，可以在前束中将存在量词消去，而不影响公式的永假性。而不影响公式的永假性。2023/5/1142Skolem标准型标准型p通过变换通过变换消去存在量词消去存在量词所得到的公式称为所得到的公式称为Skolem标准型标准型，而拿来代替存在量词
37、的变量的函数称，而拿来代替存在量词的变量的函数称Skolem函数函数。无参。无参Skolem函数有时称函数有时称Skolem常常量量。从一阶逻辑的公式变换到从一阶逻辑的公式变换到Skolem标准型标准型不是不是等等值变换，因为值变换，因为Skolem标准型与原公式不等值。但标准型与原公式不等值。但它们保持永假性。它们保持永假性。2023/5/1143合适公式的标准化合适公式的标准化p1、标准化需求、标准化需求n常见的基于谓词演算的推理：常见的基于谓词演算的推理：归结反演归结反演、(正向正向/逆向逆向)演绎推理演绎推理p要求以要求以量词前束范式量词前束范式来表示合适公式来表示合适公式n量词前束范
38、式量词前束范式形式如下：形式如下：p(Q1x1)(Q2x2)(Qkxk)M，其中，其中pM母式，不包括任何量词；母式，不包括任何量词；pQixiQi可以是可以是量词量词符号符号 或或；xi是量词的是量词的约束变量约束变量(i=1,2,k)n归结反演归结反演要求要求M标准化为标准化为合取范式合取范式，定义如下：，定义如下：pM=W1 W2 WnpWi=Li1 Li2 Lim(i=1,2,n)pLij=Pij|Pij:文字（文字（Literal），是，是谓词公式谓词公式Pij或或其取反其取反2023/5/1144p2、合取范式的标准化过程、合取范式的标准化过程n应用应用合适公式性质合适公式性质将公
39、式逐步转化的过程。将公式逐步转化的过程。n转化步骤没有严格的规定转化步骤没有严格的规定n较合理的化简过程，分为较合理的化简过程，分为8步：步：p消去多余的量词（很少出现）；消去多余的量词（很少出现）；p消去蕴涵符号；消去蕴涵符号；p减少否定的辖域（内移否定符号）；减少否定的辖域（内移否定符号）；p变量标准化（变量换名）；变量标准化（变量换名）；p消去存在量词消去存在量词 (Skolem变换变换)；p全称量词前束化（化为前束形）；全称量词前束化（化为前束形）；p消去全称量词；消去全称量词；p把把母式母式转化为转化为合取范式合取范式。2023/5/1145p2、合取范式的标准化过程、合取范式的标准
40、化过程p消去多余的量词（很少出现）消去多余的量词（很少出现）n若若一个量词的辖域内并未出现量词的约束变一个量词的辖域内并未出现量词的约束变量量，则该量词是多余的，应该删除；，则该量词是多余的，应该删除；n例，例，(x)P(y)，则，则(x)可以消去，得到可以消去，得到P(y)；n正常情况下，合适公式中不应出现多余的量正常情况下，合适公式中不应出现多余的量词。词。p消去蕴涵符号消去蕴涵符号n蕴涵式转化蕴涵式转化：PQ P Q；n例，例，Q(x,y)P(y)Q(x,y)P(y)。2023/5/1146p2、合取范式的标准化过程、合取范式的标准化过程p内移否定符号内移否定符号n使否定只出现在原子谓词
41、公式前，构成使否定只出现在原子谓词公式前，构成否定文字否定文字；n狄狄.摩根定律：摩根定律：p(P Q)P Qp(P Q)P Qn双重否定：双重否定：(P)Pn量词否定：量词否定：p(x)P(x)(x)(P(x)p(x)P(x)(x)(P(x)n例，例，(y)P(y)P(f(x,y)(y)P(y)P(f(x,y)p变量换名变量换名n“全称量词前束化全称量词前束化”后，同名变量的辖域无法区分，所后，同名变量的辖域无法区分，所以为避免差错，必须换名；以为避免差错，必须换名；n约束变量的虚元性约束变量的虚元性进行变换；进行变换；(x)p(x)=（x）Q（x）标准化而得到（标准化而得到（x）p(x)=
42、（y）Q（y）2023/5/1147p2、合取范式的标准化过程、合取范式的标准化过程p消去存在量词（消去存在量词（Skolem变换变换）n 在在 的辖域内的辖域内p(z)(w)Q(x,z)P(z,w)pw依赖于依赖于z，由函数，由函数w=g(z)来定义这种依赖关系；来定义这种依赖关系；p用用g(z)来取代约束变量来取代约束变量w，消去存在量词，消去存在量词 w；p(z)Q(x,z)P(z,g(z)n 在在多个多个 的辖域内的辖域内p(x)(y)(z)(w)P(x,y,z,w)p用多元函数用多元函数g(x,y,z)来取代约束变量来取代约束变量w，消去存在量词，消去存在量词 w；p(x)(y)(z
43、)P(x,y,z,g(x,y,z)n 在在 的辖域外的辖域外p(w)(z)Q(x,z)P(z,w)p用用任意常量任意常量A取代约束变量取代约束变量w，消去存在量词，消去存在量词 wp(z)Q(x,z)P(z,A)前两种叫前两种叫Skolem函数，第三函数，第三种叫种叫Skolem常量常量2023/5/1148总结：总结：Skolem函数函数和和Skolem常量常量在消去存在量词的过程中，需要用到在消去存在量词的过程中，需要用到Skolem函数或函数或Skolem常量。若常量。若存在量词是在全称量词的辖域内存在量词是在全称量词的辖域内，用用Skolem函数消去存在量词函数消去存在量词。Skole
44、m函数所使用函数所使用的函数符号必须是的函数符号必须是新的新的，即不允许是公式中已经出现，即不允许是公式中已经出现过的函数符号。过的函数符号。若要消去的若要消去的存在量词不在任何一个全称量词的辖域内存在量词不在任何一个全称量词的辖域内，用不含变量的用不含变量的Skolem函数即函数即Skolem常量消去存在量常量消去存在量词词。所使用的常量符号必须是。所使用的常量符号必须是新的新的，它未曾在公式其，它未曾在公式其他地方使用过。他地方使用过。Skolem变换变换不是等价变换，但变换前后的值永假性不是等价变换，但变换前后的值永假性保持不变保持不变。2023/5/1149p2、合取范式的标准化过程、
45、合取范式的标准化过程p全称量词前束化全称量词前束化n经过经过“变量换名变量换名”后，所有量词的约束变量均有后，所有量词的约束变量均有不同的名字；不同的名字；n只要简单地将只要简单地将 移到合适公式的最前面；移到合适公式的最前面；n约束变量的作用范围不会变化。约束变量的作用范围不会变化。p消去全称量词消去全称量词n经过经过“消去存在量词消去存在量词”后，所有变量均受后，所有变量均受 的约束；的约束；n简单地删除简单地删除，只留下母式。，只留下母式。p把母式转化为把母式转化为合取范式合取范式n分配律分配律：P(Q R)(P Q)(P R)2023/5/1150p2、合取范式的标准化过程、合取范式的
46、标准化过程n例、化简合适公式例、化简合适公式(x)P(x)(y)P(y)P(f(x,y)(y)(w)Q(x,y)P(y,w)2023/5/1151p2、合取范式的标准化过程、合取范式的标准化过程n例、化简合适公式例、化简合适公式(x)P(x)(y)P(y)P(f(x,y)(y)(w)Q(x,y)P(y,w)消去蕴涵符号消去蕴涵符号(x)P(x)(y)P(y)P(f(x,y)(y)(w)Q(x,y)P(y,w)2023/5/1152p2、合取范式的标准化过程、合取范式的标准化过程n例、化简合适公式例、化简合适公式(x)P(x)(y)P(y)P(f(x,y)(y)(w)Q(x,y)P(y,w)内移
47、否定符号内移否定符号(x)P(x)(y)P(y)P(f(x,y)(y)(w)Q(x,y)P(y,w)2023/5/1153p2、合取范式的标准化过程、合取范式的标准化过程n例、化简合适公式例、化简合适公式(x)P(x)(y)P(y)P(f(x,y)(y)(w)Q(x,y)P(y,w)变量换名变量换名(x)P(x)(y)P(y)P(f(x,y)(z)(w)Q(x,z)P(z,w)2023/5/1154p2、合取范式的标准化过程、合取范式的标准化过程n例、化简合适公式例、化简合适公式(x)P(x)(y)P(y)P(f(x,y)(z)(w)Q(x,z)P(z,w)消去存在量词消去存在量词P(A)(y
48、)P(y)P(f(A,y)(z)Q(A,z)P(z,g(z)2023/5/1155p2、合取范式的标准化过程、合取范式的标准化过程n例、化简合适公式例、化简合适公式P(A)(y)P(y)P(f(A,y)(z)Q(A,z)P(z,g(z)全称量词前束化全称量词前束化(y)(z)P(A)P(y)P(f(A,y)Q(A,z)P(z,g(z)2023/5/1156p2、合取范式的标准化过程、合取范式的标准化过程n例、化简合适公式例、化简合适公式(y)(z)P(A)P(y)P(f(A,y)Q(A,z)P(z,g(z)消去全称量词消去全称量词P(A)P(y)P(f(A,y)Q(A,z)P(z,g(z)20
49、23/5/1157p2、合取范式的标准化过程、合取范式的标准化过程n例例3、化简合适公式、化简合适公式P(A)P(y)P(f(A,y)Q(A,z)P(z,g(z)把母式转化为把母式转化为合取范式合取范式P(A)P(y)Q(A,z)P(z,g(z)P(f(A,y)Q(A,z)P(z,g(z)完成标准化过程！完成标准化过程！2023/5/1158归结演绎推理归结演绎推理p自动定理证明一般表示形式为：自动定理证明一般表示形式为：pF1 F2 FnWnF1,F2,Fn都是合适公式，表示都是合适公式，表示公理公理或或事实事实；nW是合适公式，表示是合适公式，表示待证明的定理待证明的定理，称为，称为目标公
50、式目标公式；p证明的方法可分两大类：证明的方法可分两大类：n演绎法演绎法p直接证明直接证明F1 F2 FnW为为永真永真；n反证法反证法p间接证明间接证明(F1 F2 FnW)为为永假永假；p证明证明F1 F2 Fn W的的永假永假n即即F1,F2,Fn W是一个矛盾集。是一个矛盾集。2023/5/1159归结演绎推理归结演绎推理p海伯伦（海伯伦（HerbrandHerbrand）n提出的提出的H H域（海伯伦域）域（海伯伦域）和和海伯伦定理海伯伦定理；n为为自动定理证明自动定理证明奠定了理论基础；奠定了理论基础；p鲁宾逊（鲁宾逊（RobinsonRobinson）n提出的提出的归结原理归结原