资源预览内容
第1页 / 共15页
第2页 / 共15页
第3页 / 共15页
第4页 / 共15页
第5页 / 共15页
第6页 / 共15页
第7页 / 共15页
第8页 / 共15页
第9页 / 共15页
第10页 / 共15页
亲,该文档总共15页,到这儿已超出免费预览范围,如果喜欢就下载吧!
资源描述
4.5 一阶谓词语义系统4.5.1 什么是形式系统语义抽象公理系统或者形式系统,具有较高的抽象性。因此,已经脱离了任何一个具体的系统,但是我们可以对形式系统作出各种解释。通过这种解释将形式系统对应到各种具体的系统中取。例如可以将一阶谓词逻辑系统,解释到平面几何系统中。怎样将形式系统解释成具体系统呢?我们先看下面的例子:如果我们要知道的具体的真值=1,我们至少要知道以下事情:1、 x在什么范围之内,x范围是实数。2、 f是什么? (X+1)3、 P是什么?P代表的是大于04、 a=?a=15、 x=?,x5,4例如,我们可以作出以下解释:1、解释1:l x在实数中取值l P表示等于0l 表示x-al a=5因此,公式解释为。令x=5, 则s(x) -5s(f(a,x) -I(f)(I(a),s(x)令x=6,则2、解释2:l x在实数中取值l P表示大于等于0l 表示因此,公式解释为。这个公式不必对a和x作出具体解释,就可以确定公式的真值。即对于任何实数x,和赋值映射v,。由上面的例子可以看出,要对形式系统作出解释,我们要了解以下问题: x取值于哪里?即规定讨论问题的领域。 给出谓词的含义和谓词的真值 给出函数的解释 给出变量和常量的值 根据连接词的赋值规则,赋值这就是我们要研究的语义系统指称语义的主要内容。现代逻辑语义学理论的创始人是美籍波兰逻辑学家、哲学家A. Tarski,其奠基性文章是他在1933年发表的形式语言中的真实概念。后来被称为模型论标准语义学理论。进一步的发展由维特根斯坦最早提出设想,卡尔纳普最早把它展开为系统。这体现在他1947年发表的 意义和必然性一书中;卡普兰克里普克(S.kripke)和蒙太古作出了进一步的贡献,提出了非经典逻辑的语义学理论模态逻辑语义学(克里普克结构)。4.5.2 形式语义基本概念1、 指称语义:语义是由语义结构和以及在这种结构下公式赋真值的规定构成的。2、 语义结构:对于抽象公理系统或形式系统作出的一种解释。包括个体域和在这种个体域上的个体运算和个体间关系。下面给出形式系统语义的定义:3、 形式语义:设FS是已经存在的形式系统,FS的语义有语义结构和赋值两个部分组成:a) 语义结构:当FS的项集TERM不为空时,由非空集合U和规则组I所组成二元组(U,I),称为形式系统FS的语义结构。其中U和I的性质如下:i. U为非空集合,称为论域或者个体域;ii. 规则组I,称为解释,根据规则组的规定对项集TERM中的成员指称到U中的个体;规定对原子公式如何指称到U中的个体性质(U的子集)、关系(的子集)。b) 指派:若形式系统FS中的变量集合Variables非空,那么下列映射称为指派:s:variblesU。对于给定的语义结构,可以将指派扩展到项集TERM上:TERMU; S(t) 当t 为变元 S指派t中变元由解释确定 当t为非变元 F(x,a) = I(f) (x, I(a) = s1( I(f) (x, I(a) = I(f) (s(x), I(a)P(f(a,x) =I(P)(I(f)(a,s(x)c) 赋值:是指一组给公式赋值的规则,据此规则可对每一结构U和指派S确定一由原子公式到值域的映射v:atomicvalue。根据这个赋值规则,可以将赋值映射进行扩展:v为:d) 可满足:公式A称为可满足,如果存在结构S与指派s,使一个赋值映射v满足v(A)=1,否则为不可满足。|=P(f(x,y)F(x,y) s(x,y)=(1,2) s(f(x,y)=I(f)(1,2)=I(f)(s(x),s(y)V(P(x,y)=V(I(P)(s(x),s(y)V(I(Q)(s(x)4.5.3 一阶谓词语义1、语义结构:一阶谓词形式系统采用TARSKI语义结构。这种语义结构以为其真值集合。每一个Tarski语义结构S,由非空集合U和下列解释I构成:i 常元:对于任一常元a, I(a)U, I(a)记为,为论域中的一个元素;ii 函数: 对于任一n元函数为U的一个n元函数,记为:;iii 谓词:对于任一n元谓词,为U上的一个n元关系,记为,。当n=1时,为U的子集。2、指派:指派S为变元集合到上的映射。S可以扩展为:F(a,x)S(x)=5S(f(a,x)=I(f)(I(a),S(x)= I(f)(I(a),5)i 对于每一变元v:;ii 对于每一常元a:;iii 对于每一个n元函词fn和项t1,t2.tn:S(F(x1,x2)=F(S(x1),S(x2)由此可见,指派与结构无关,而与结构相关。3、赋值:i 赋值映射v:Atomic定义为:对任何n元谓词及项t1tn,当且仅当,其中。Y=X+1P(x,y), I(P)=, , s(x)=3, s(y)=2?; I(P)(s(x),s(y):P()=1ii 赋值映射v按下列规则扩展,:l 对原子公式A:;l 对于公式,当且仅当;l 对于公式,当且仅当或;l 对公式,当且仅当对于U中每一元素d, ,其中表示指派S对x指派元素d。4、所有公理为永真式:我们从公理中取公理5来证明,即证明|=为永真式。已知:=1求证:=1任意取一个结构,和这个结构任意一个指派,对于任意一个赋值f,满足f()=1,则f()=1.任意取一个结构,一个赋值映射f,f满足f()=1:证明:f()=1.f()=1, f()=1,证明:f()=1D, B(d)=1;f(AB)(d)=1 f(A(d)B(d)=1; f(A)(d)=1f(A(d)=0,或者f(B(d)=1;f(A)(d)=1 f(B(d)=1对于论域中的任意一个个体,d, f(A(d)B(d)=1, f(A(d)=1, F(B(d)=1 f( (A(Sx|d)B(Sx|d) =1 A(d)=1,A(d)B(d)对于论域中的任意一个个体,d, f(A(Sx|d)1求证:对于论域中的任意一个个体,d, f(B(Sx,|d)1证明:只要证明对任意结构U和指派S,对于任一赋值v:成立。由演绎定理可知,要证明,则只需证明:。因此,只需证明对于任意结构U和指派S,如果U和S满足:和成立;则在结构U和指派S下在S和U下成立。只需对任意元素d,进行验证:对于和任意赋值v由于:(1)已知(2)已知由(1)可知,或者或者。由(2)可知,因此。因此,命题成立。5、语义构造的例子一阶谓词形式系统的语义结构为:只有一个函词、一个谓词和一个常元的形式系统(推理和符号与一阶谓词相同)。P2, f1,a个体域:,即自然数集合N谓词:为N上的关系。函词:为N上的后继,即常元:判断以下公式的真值:=1 v1v2P(v1+1,v2)=1P(x1+1, x1+2)=04.6 一阶元理论4.6.1 语法构成对于一阶谓词形式系统的语法构成,主要有以下定理: 独立性:FSFC的公理集合是独立的。 一致性:FSFC是一致的,即不存在FSFC的公式A,使A及同时成立 FSFC是不完全的,即存在FSFC的公式A,使A及都不成立。只需证明对于原子公式P(x), P(x), 均不成立。* FSFC的不一致扩充为完全的。A4 -(A-(B-A) 半可判定性:FSFC是半可判定的,即存在一个机械的实现过程,能对FSFC中的定理作出肯定判断,但对非定理的FSFC公式未必能作出否定判决。推广:设为FSFC的一个可判定公式集(递归集),那么的演绎结果集合是半可判定的。4.6.2 语义结构对于一阶谓词形式系统的语义主要有以下定理: 紧致性:对FSFC的任何公式集合,如果的所有有穷子集可满足,那么也是可满足的。证明:同命题逻辑。反证法4.6.3 语法语义关系语法语义关系,主要有以下定理: 合理性:对于FSFC中任一公式A,如果A,那么|=A。合理性推广:对于FSFC的任一公式集和公式A,若A,则|=A。证明简单,与命题逻辑基本相同。合理性推论:对于FSFC中任意公式A,B,若AB,则A|=B 完备性:对于FSFC的任一公式A,如果|=A,那么A。Godel完备性定理:对于FSFC的任一公式集和公式A,如果|=A,则A。已知:对于任意的结构,和任意的赋值映射f,如果f使得f()=1,则f(A)=1.求证:存在一个证明序列A1,An=A,其中Ai或者为公理,或者为中的元素,或者是由前边的通过推理规则得到。证明:对于FSFC的任一公式集是一致的,充要条件为是可满足的。完备性定理又被称为Godel完备性定理,其证明思路如下:(1) 对于一阶谓词任意公式集合是一致的,则存在一个一致公式集合,满足如果公式集合K包含,且K是一致的,则。成为的最大一致扩充。A1,A2,A3=A1,A2,A3,A4=f(A1,A2,A3)=1;f(A)=1;f1(A1,A2,A3,A4,A)=1;F1(A)=1(2)对于的最大一致扩充和公式A,如果A,则有。(3)反证法:假设A ,故有A,从而为一致的。由(1)可知,存在着一极大一致集F,使得AF(或者AF)。根据前提|=A ,F|=A。由(2)可知F。这与F的一致性矛盾。 5 归结原理及应用5.1 标准形式公式标准化的主要目的是对公式进行机械化推理过程。机械化推理过程,是知识工程、逻辑程序设计、人工智能和定理机器证明等理论的基础。在讲述公式标准化过程之前,我们首先介绍整个形式逻辑的基本发展思路。推理过程: 语义 逻辑推理 反证,真值表合理、完备 公式形式系统 公理,规则(分离规则)(机器难以识别)同可满足 标准形式标准形式 ,代替(机械化)B:B A,A =0假设公式集合S=A1,A2,.,An,假设T=B1,B2,B3,.,Bm这是标准型,这个标准型T和S之间是同可满足的。如果S是可满足的,则T是可满足的。如果T是不可满足的,则S是不可满足的。, x=3, B RETE=NETWORK 1965 HPROLOG , 1982 :RULE ENGINE-ILOG目标:反向推理B, B 0:一个集合F化简到标准型S,如果集合F是可满足的,则标准型S是可满
网站客服QQ:2055934822
金锄头文库版权所有
经营许可证:蜀ICP备13022795号 | 川公网安备 51140202000112号