人工智能117精编版

《人工智能117精编版》由会员分享，可在线阅读，更多相关《人工智能117精编版（118页珍藏版）》请在金锄头文库上搜索。

1、自 动 定 理 证 明 Automated Theorem Proving,软件形式化与自动推理学科组 2010年10月,1、自动定理证明理论及方法 2、基于tableau的自动定理证明,自动定理证明理论及方法,1、命题逻辑自动定理证明方法 2、一阶谓词逻辑自动定理证明方法,古典数理逻辑 命题逻辑:一句有真假意义的话。(真值:T和F) 是谓词逻辑的一种简单情形。 简单命题（原子命题）：不包含联结词的命题。 复合命题：两个或几个简单命题用联结词联结构成 的命题。 谓词逻辑:,1 命题逻辑,1.1 命题联结词及真值表,否定：,析取：,合取：,1.1 命题联结词及真值表,合式公式：命题演算的合式公式

2、，规定为： （1） 单个命题变元本身是一个合式公式； （2） 如果A是合式公式，那么 A也是合式公式； （3） 如果A，B是合式公式，那么AB, AB，AB，AB都是合式公式； （4）iff 能够有限次应用(1)、(2)、(3)所得到的包含命题变元、联结词和括号的符号串是合式公式。,定义,1.2 重言式,重言式（永真式）：如果一个公式，对它的任一解释I下其真值都为真。 PP,定义,一个公式，如有某个解释I0，在I0下给公式真值为真，则称这公式是可满足的。 重言式是可满足的。矛盾式是不可满足的。,1.2 重言式,重言式、矛盾式和不可满足的公式关系：,公式A永真，当且仅当A永假； 公式A可满足，当

3、且仅当A非永真； 不可满足的公式必永假； 不是永假的公式必可满足。,1.3 命题形式化,形式化,一些推理问题的描述,常以自然语句来表示: 把自然语言形式化成逻辑语言,即以符号表示的逻辑公式； 根据逻辑演算规律进行推理演算。,归结法是定理机器证明的重要方法； 是仅有一条归结推理规则的机械推理法； 从而易于程序实现； 可推广到谓词逻辑的推理。,1.4 归结推理法,1.5 tableau推理法（1）,tableau定义,令A1,An为一命题公式的有限集合： 1、下列分支为A1,An的一个tableau A1 An 2、如果T是一个A1,An的tableau，对T应用tableau扩展规则生成T*，那

4、么T*仍然是一个tableau。,1.5 tableau推理法（2）,命题hintikka集定义,一个命题公式集合H称为Hintikka集，如果： 1、对于任何命题字母AH,不同时存在AH 2、FH; TH; 3、ZH ZH; 4、H 1H并且2H 5、H 1H或者2H,谓词逻辑:是命题逻辑的推广，命题逻辑是谓词逻辑的特殊情况。因为任何一个命题都可以通过引入具有相应含义的谓词（个体词视为常量）来表示，或认为命题是没有个体变元的零元谓词。 函数：函数不单独使用，是嵌入在谓词中，用小写字母表示。 father(x): 表示x的父亲； P(x): 表示x是教师； P(father(x): 表示x的父

5、亲是教师。,2 一阶谓词逻辑,量词:用来表示个体数量的词，对个体所加的限制、约束的词。 符号：全称量词，：存在量词。 凡事物都是运动的。 (x)(x是运动的） (x)(P(x):当且仅当对论域中的所有x来说，P(x)均为真时方为真，这就是全称量词的定义。当且仅当有一个x0D,使P(x0)=F时，(x)(P(x)=F。,2 一阶谓词逻辑（2）,2.1 自然语言的形式化,1、所有的有理数都是实数。 (x)(P(x)Q(x) 2、函数f(x)在a,b上的点x0处连续。 ()(0()(0(x)(|x-x0|f(x)-f(x0)| ),3、设Tony、Mike和John属于ALPINE俱乐部，ALPIN

6、E俱乐部的成员不是滑雪运动员就是登山运动员。登山运动员不喜欢雨，而且任何不喜欢雪的人都不是滑雪运动员。Mike讨厌Tony所喜欢的一切东西，而喜欢Tony所讨厌的一切东西。Tony喜欢雨和雪。,2.2 合一算法,替换：是形如t1/v1,tn/vn的一个有限集合，其中vi是变量符号，ti是不同于vi的项，并且在此集合中没有在斜线符号后面有相同变量符号的两个元素。称ti为替换的分子，vi为替换的分母。,合一：替换称为表达式集合E1,Ek的合一，当且仅当E1 = E2 = Ek 。表达式集合E1,Ek称可合一的，如果存在关于此集合的一个合一。,表达式集合P(a,y), P(x,f(b)是可合一的，其

7、合一为 =a/x, f(b)/y,2.3 一阶谓词归结推理(1),假设有以下前提知识： （1）自然数是大于零的整数； （2）所有整数不是偶数就是奇数； （3）偶数除以2是整数。 求证：所有自然数不是奇数就是一半为整数的数。,（3）把F1、F2、F3和G化成子句集。 N(x)GZ(x) N(u)I(u) I(y)E(y)O(y) E(z)I(S(z) N(t) O(t) I(S(t),2.3 一阶谓词归结推理(2),用归结的方法回答问题：“有没有ALPINE俱乐部的一个成员，他是一个登山运动员但不是一个滑雪运动员？”,Sportman(x,Snow)Sportman(x,Mountain) Sp

8、ortman(x,Mountain)Like(x,Rain) Like(x,Snow)Sportman(x,Snow) Like(Mike,Rain) Like(Mike,Snow) Like(x,Snow)Like(x,Rain),ANSWER(x),2.3 一阶谓词归结推理(3),(1) 定义谓词 theif(x):表示x是贼； likes(x,y):表示某人x喜欢某物y; may_steal(x,y):表示某人x可能会偷某物y。,(2)将已知事实表示成谓词公式,并化成子句集 theif(John) likes(Paul,wine) likes(Paul,cheese) likes(Pau

9、l,y)likes(John,y) theif(x)likes(x,y)may_steal(x,y) may_steal(John,Z)ANSWER(Z),(3)归结 theif(John)likes(John,y)ANSWER(y) 归结,=John/x, y/z likes(John,y)ANSWER(y) 归结 likes(Paul,y)ANSWER(y) 归结 ANSWER(wine) 归结,=wine/z ANSWER(cheese) 归结,=cheese/z,所以John可能会偷窃wine,也可能会偷窃cheese。,2.3 一阶谓词归结推理(4),作业,2.3 一阶谓词归结推理(

10、5),作业,2.3 一阶谓词归结推理(6),作业,2.4 一阶谓词tableau推理(1),2.4 一阶谓词tableau推理(2),(1) (x)P(x)Q(x)(x)P(x)(x)Q(x) (2) (x)P(x)Q(x) (3) (x)P(x)(x)Q(x) (4) (x)P(x) (5) (x)Q(x) (6) Q(c) (7) P(c) (8) P(c)Q(c) (9) P(c) (10) Q(c) * *,2.4 一阶谓词tableau推理(3),自由变量tableau,(x),(f(x1,xn),对于一个自由变量x,f为一个Skolem化的函数, x1,xn是所有的tableau中

11、的自由变量,一阶tableau扩展规则,=v1/a, v2/b(a), v3/f(b(a),a),2.4 一阶谓词tableau推理(4),含等词tableau,自反规则:句子tt加到子句集S的tableau的任何一个分枝末尾产生另一个tableau这里t是Lpar的任何项直观表示为： t t 替换规则如果tu和(t)产生在S的tableau分枝上，(u)被加到tableau后，产生另一个tableau这里t和u是Lpar的任何封闭项 tu (t) (u),2.5 tableau推理应用(1),数据库修正,给定一个数据库实例r和一个完整性约束集合IC对于IC和r的tableau，TP(ICr)

12、是一个以公式集ICr为根节点的推理树，每个tableau分枝B为Ir形式，ITP(IC)，I称为分枝的IC部分，如果r是不相容的，tableau是封闭的，即tableau存在封闭分枝由于IC是相容的，因此一个tableau的IC部分永远是不封闭的，只有r和IC相结合才能产生一个封闭的tableau。,2.5 tableau推理应用(2),自然语言理解,Mary is married. She has no husband.,2.5 tableau推理应用(3),电路仿真,门电路及其类事实： xor_gate(g1). xor_gate(g2). and_gate(g3). and_gate(g

13、4). or_gate(g5).,所有连接类事实： connecttion(in(1, f1), in(1, g1). connecttion(in(2, f1), in(2, g1). connecttion(in(1, f1), in(1, g3). connecttion(in(2, f1), in(2, g3). connecttion(in(3, f1), in(1, g4). .,基于tableau的自动定理证明,（4）重要的自动推理方法：从二十世纪六十年代开始，特别是近十年，引起了计算机科学家的广泛兴趣。,（3）通用性和直观性：对于不同的逻辑系统，使用相同的tableau规则，只

14、是对公式构造集进行扩展，使之更接近相应的逻辑系统 。,（2）引入相应的谓词，将二元关系的性质用逻辑公式来表示。,（1）将语义结构中的二元关系显式地表现出来。,1.,引言,1.1 tableau实质,1.2 Tableau方法回顾,1.3 研究的意义,人工智能研究的基础工作，许多重要的人工智能系统，都以推理系统为其核心部分。,对人工智能的其它分枝产生深远的影响，提出的推理方法已被应用于人工智能的各个领域。,专家系统 问题解答系统 学习系统 程序的自动综合与合成 医疗系统 信息检索,1.4 研究现状,含量词tableau改造技术,Fitting提出了循环控制-规则应用次数h的技术。,increat

15、e_prove(Fml，H) :prove（Fml， ， ， ，H） increate_prove(Fml，H) :NewH is H+1，H=VarLim， increate_prove（Fml，NewH）。,(1)相关技术和策略的研究,非相关部分剪枝技术,由Oppacher提出的tableau压缩技术。,j,N,:,:,封闭,没用,封闭,B,B,tableau非相关部分剪枝技术,因子分解技术,因子分解技术作为模型删除而引入。,p,q,N3,N2,p,q,q,p,N1,N4,因子分解技术实现公式集pq,pq,pq,pq的证明过程,1.4 研究现状,子句tableau方法 超tableau方法 决策图tableau方法 翻译成整数规划的tableau方法,(2)理论和方法的研究,1.4 研究现状,直觉逻辑 模态逻辑 多值逻辑 非单调逻辑,(3)非经典逻辑扩展的研究,数据库修正 完整性检查 查询和变更数据库记录,(1)数据库方面的应用,1.5 tableau应用,1.5 tableau应用,使用超tableau推理的观点来解决诊断问题。 实现了基于tableau的诊断系统 NIHIL,(2)诊断方面的应用,利用