逻辑表示及归结系统

逻辑表示及归结系统

ID:27559910

大小:607.51 KB

页数:49页

时间:2018-12-04

逻辑表示及归结系统_第1页
逻辑表示及归结系统_第2页
逻辑表示及归结系统_第3页
逻辑表示及归结系统_第4页
逻辑表示及归结系统_第5页
资源描述:

《逻辑表示及归结系统》由会员上传分享,免费在线阅读,更多相关内容在教育资源-天天文库

1、第6章基于谓词逻辑的归结方法一阶谓词逻辑概述归结原理归结反演系统基于归结法的问题求解定义:逻辑学是研究人类思维活动规律的科学.方法:利用数学(符号化、公理化、形式化)的方法来研究这些规律.作用:是表达人类思维和推理的最精确和成功的方法,成为AI的重要基础.表现方式和人类自然语言非常接近便于计算机做精确处理分类:经典逻辑和非经典逻辑两大类,经典逻辑中命题逻辑和一阶谓词逻辑是基础.1一阶谓词逻辑概述命题的定义:表示知识的陈述性形式或具有真假意义的陈述句.例:A:张平是学生;B:树叶是绿色的;命题的类型:原子命题:表达单一意义、不能再分

2、解.如P:天在下雨;Q:天晴复合命题:由连接词、标点和原子命题构成.如,P→~Q可表示:如果天在下雨则天不晴.命题逻辑就是研究命题与命题之间关系的符号逻辑系统,包含语法、语义、演算等.1.1命题概念原子命题是命题逻辑中最基本的单元,不能对其进行分解,也不能对其结构进行分析.引发的问题:限制了它的使用;为了突破这种束缚,发展了谓词逻辑.原子命题可分解;以命题中的谓词为基础进行分析研究.1.2谓词概念原子命题分解为谓词、个体2部分。例:1、3是质数,x是质数,F(x);2、王二生于武汉市,x生于y,G(x,y);3、7=23,x=y

3、z,H(x,y,z);3、王二、武汉市、7等,称为个体(具体);代表个体的变元,称为个体变元(抽象);刻画个体性质或个体之间关系的词叫谓词,如“是质数”、“生于”、“…=……”谓词中包含的个体数目称为谓词的元数.在谓词P(x1,x2,…,xn)中,若每个xi都是个体常量、变元或函数,则称它为一阶谓词,若某个xi本身又是一个一阶谓词,则称它为二阶谓词…谓词与命题的区别——更强的表达能力1、有概括能力例如,是一个城市,谓词CITY(X)2、可表示变化着的情况命题值是恒真或恒假,谓词值可因参数而异3、可在不同的知识之间建立高级联

4、系HUMAN(X)X是人,LAWED(X)X受法律约束,COMMIT(X)X犯法,PUNISHED(X)X受法律制裁HUMAN(X)→LAWED(X)人人都要受法律约束COMMIT(X)→PUNISHED(X)犯罪,就要受惩罚{[HUMAN(X)→LAWED(X)]→[COMMIT(X)→PUNISHED(X)]}2归结原理定理证明:已知一公式集F1,F2,…,Fn,要证明一个公式W是否成立,即要证明W是公式集的逻辑推论.方法:直接法:F1F2…Fn→W是永真式.间接法(反证法):F1F2…Fn~W为永假基本思想:采

5、用反证法将待证明的表达式转换为逻辑公式,然后再进行归结,归结能够顺利完成,则证明原定理是正确的.2.1归结原理概述2.1归结原理概述(续)理论依据:空子句:一种没有任何解释能满足的子句,其取值总是假,简记为□或NIL.用归结法从子句集S导出的扩大子句集S1(S∪归结式),其不可满足性是不变的.(待证)技术思路:设法检验原(或扩充的)子句集S是否含有空子句,若S集中存在空子句,则表明S为不可满足的.过程:S→S1→S2→…→Sn归结过程可以一直进行下去,也就是要通过归结过程演绎出S的不可满足性来,从而使定理得到证明.几个概念不含有任

6、何连接词的命题(谓词)公式称为原子公式(原子).原子或原子的否定统称为文字.子句是由一些文字组成的析取式.不包含任何文字的子句称为空子句.(不能用任何解释所满足)子句构成的集合,称为子句集.2.2命题逻辑的归结法1)归结式的定义及性质归结:设C1与C2是子句集中的任意两个子句,如果C1中的文字L1与C2中的文字L2互补,那么从C1和C2中分别消去L1和L2,并将两个子句中的余下部分析取,构成一个新的子句C,这一过程称为归结.C:C1和C2的归结式;C1和C2:C的亲本子句.没有互补对的两子句没有归结式。[例]设C1=~PQR,

7、C2=~QS,C1中L1=Q与C2中L2=~Q互补.得:C=~PRS[例]设C1=P,C2=~PP与~P互补,可得:C=□.[例]设C1=~PQ,C2=~QR,C3=P,首先对C1,C2进行归结,得C12=~PR,再对C12,C3归结,得C123=R.定理:两个子句C1和C2的归结式C是C1和C2的逻辑结论.(即C1C2C)证明:设C1=LC1',C2=(~L)C2',通过归结可得到C=C1'C2'因为C1=LC1'=C1'L~C1'L;C2=~LC2'LC2'C1C2=(~C1'L)(

8、LC2')由假言三段论得到:(~C1'L)(LC2')(~C1'C2')而~C1'C2'C1'C2'=CC1C2C[证毕]推论:子句集合S={C1,C2,…,Cn}与S1={C,C1,C2,…,Cn}的不可满足性是等价的(C

当前文档最多预览五页,下载文档查看全文

此文档下载收益归作者所有

当前文档最多预览五页,下载文档查看全文
温馨提示:
1. 部分包含数学公式或PPT动画的文件,查看预览时可能会显示错乱或异常,文件下载后无此问题,请放心下载。
2. 本文档由用户上传,版权归属用户,天天文库负责整理代发布。如果您对本文档版权有争议请及时联系客服。
3. 下载前请仔细阅读文档内容,确认文档内容符合您的需求后进行下载,若出现内容与标题不符可向本站投诉处理。
4. 下载文档时可能由于网络波动等原因无法下载或下载错误,付费完成后未能成功下载的用户请联系客服处理。