人工智能自动定理证明课件

自动定理证明

AutomatedTheoremProving1、自动定理证明理论及方法2、基于tableau的自动定理证明自动定理证明理论及方法1、命题逻辑自动定理证明方法2、一阶谓词逻辑自动定理证明方法古典数理逻辑命题逻辑:一句有真假意义的话。(真值:T和F)

是谓词逻辑的一种简单情形。

简单命题（原子命题）：不包含联结词的命题。

复合命题：两个或几个简单命题用联结词联结构成的命题。谓词逻辑:1命题逻辑1.1命题联结词及真值表P

PFTTF否定：PQP∨QFFFFTTTFTTTT析取：PQP∧QFFFFTFTFFTTT合取：FTFTFTTFFTTTPQPQ蕴涵：FTFFFTTFFTTTPQPQ等价：1.1命题联结词及真值表合式公式：命题演算的合式公式，规定为：（1）单个命题变元本身是一个合式公式；（2）如果A是合式公式，那么﹁A也是合式公式；（3）如果A，B是合式公式，那么A∧B,A∨B，A→B，A

B都是合式公式；（4）iff能够有限次应用(1)、(2)、(3)所得到的包含命题变元、联结词和括号的符号串是合式公式。定义1.2重言式重言式（永真式）：如果一个公式，对它的任一解释I下其真值都为真。

P∨﹁P定义

一个公式，如有某个解释I0，在I0下给公式真值为真，则称这公式是可满足的。重言式是可满足的。矛盾式是不可满足的。1.2重言式重言式、矛盾式和不可满足的公式关系：

公式A永真，当且仅当﹁A永假；

公式A可满足，当且仅当﹁A非永真；

不可满足的公式必永假；不是永假的公式必可满足。1.3命题形式化形式化

一些推理问题的描述,常以自然语句来表示:

把自然语言形式化成逻辑语言,即以符号表示的逻辑公式；

根据逻辑演算规律进行推理演算。

实例：如果我学习，那么我数学不会不及格；如果我不热衷于玩扑克，那么我将学习；但我数学不及格。结论：我热衷于玩扑克。解：设P:我学习Q:我数学不及格R:我热衷于玩扑克

((P→﹁Q)∧(﹁R→P)∧Q)=>R归结法是定理机器证明的重要方法；是仅有一条归结推理规则的机械推理法；从而易于程序实现；可推广到谓词逻辑的推理。1.4归结推理法归结证明过程1、证明A→B（定理）是重言式，等价于证A∧﹁B是矛盾式。使用归结法就是从A∧﹁B出发。2、建立子句集S

将A∧﹁B化成合取范式，如

P∧(P∨R)∧(﹁P∨﹁Q)∧(﹁

P∨R)

形式，子句集合为：

S={P,(P∨R),(﹁P∨﹁Q),(﹁

P∨R)}3、对S作归结对S的子句作归结（消互补对），如子句P∨R

与﹁P∨﹁Q

作归结，得归结式R∨﹁Q

,并将这一归结式放入S中，重复这过程。4、直到归结出矛盾式□。归结式的定义设C1=L∨C1’，C2=﹁L∨C2’为两个子句，有互补对L和﹁L，则新子句:

R(C1,C2)=C1’∨C2’称作C1,C2的归结式。归结推理规则归结过程就是对S的子句求归结式的过程：C1∧C2=>R(C1,C2),R(C1,C2)是子句C1,C2的逻辑推论。

从而归结是正确的推理规则。

设在任一解释下，C1和C2均为真。若在这解释下，L为真，则﹁L为假，从而必有C2’为真。于是在解释下R(C1,C2)为真。若在这解释下，﹁L为真，则L为假，从而必有C1’为真。于是在解释下R(C1,C2)为真。因此，证明了C1∧C2=>R(C1,C2)。归结推理举例((P→﹁Q)∧(﹁R→P)∧Q)=>R证明：先将((P→﹁Q)∧(﹁R→P)∧Q)∧﹁R化为合取范式

(﹁P∨﹁Q)∧(R∨P)∧Q∧﹁R建立子句集S={﹁P∨﹁Q,R∨P,Q,﹁R}归结过程：(1)﹁P∨﹁Q(2)R∨P(3)Q(4)﹁R(5)﹁P(1)(3)归结(6)

P(2)(4)归结

(7)□(5)(6)归结1.5tableau推理法（1）tableau定义令{A1,…,An}为一命题公式的有限集合：1、下列分支为{A1,…,An}的一个tableauA1

…

An2、如果T是一个{A1,…,An}的tableau，对T应用tableau扩展规则生成T*，那么T*仍然是一个tableau。Tableau扩展规则﹁

﹁ZZ﹁TFT﹁F

1

2

1

2Tableau有效性定义：一个命题公式集S是可满足的，如果某一布尔值映射到S的每个成员都为T.一个tableau分支是可满足的，如果在个上面的命题公式集是可满足的。一个tableauT是可满足的，如果至少T上的一个分支是可满足的。命题：如果任何tableau扩展规则被应用到可满足的tableau，其结果为另一个可满足的tableau．

证明．假设T是一个可满足的tableau，对于T的分枝θ应用表扩展规则产生X，生成一个tableau

T*．下面证明T*也是可以满足的．因为T是可以满足的，T至少有一个可满足的分枝，选择这一分枝，记为τ．1)τ≠θ．规则应用到θ上，τ仍为T*的分枝，因此T*是可以满足的。2)τ=θ．θ本身是可满足的，布尔赋值ν将θ中的所有公式映射为t．2a)X=α．那么θ被扩展为α1和α2而产生T*．由于α产生在θ上，有ν(α)=t，ν(α)＝ν(α1)∧ν(α2)，因此ν必将ν(α1)和ν(α2)都映射为t．这样ν将在Ｔ*的θ扩展的每个公式都映射为t，因此T*是可以满足的．2b)X=β．那么将左右儿子加到θ的最后节点上，标记为β1和β2，而产生T*，由于β产生在θ上，ν(β)=t，但ν(β)＝ν(β１)∨ν(β２)，ν将β１或β2映射为t，ν将左侧或右侧的扩展分枝映射为t．只要存在其一，T*就有可满足的分枝，因此T*是可以满足的．其它情况：X是﹁﹁Z，﹁ㄒ或﹁⊥，易证T*是可以满足的．

命题：如果公式集S存在一个tableau，那么S是不可满足的．证明．假设公式集S存在一个tableau，S是可满足的．对S构造一个开始于S封闭的tableau，由于S是可满足的，那么初始标记为S的tableau是可满足的，根据引理，S的tableau的每个子tableau都是可满足的，包括最后封闭的tableau，这显然是矛盾的，因此，S是不可满足的．

命题tableau的有效性定理：如果X有一个tableau证明，那么X是重言式．证明．

假设X有一个tableau证明但是无效的．我们推出矛盾．由于X是无效的，因此有一个模型使得﹁X为真，对X的tableau证明开始与标有﹁X的一个分枝，并且是可满足的tableau．由引理2可知，每个后继tableau都是可满足的，包括最后的封闭的tableau．但封闭的tableau不能是可满足的．因此推出矛盾．所以如果X有一个tableau证明，那么X是有效的．1.5tableau推理法（2）命题hintikka集定义一个命题公式集合H称为Hintikka集，如果：1、对于任何命题字母AH,不同时存在﹁AH．2、FH;﹁TH;3、﹁﹁ZHZH;4、

H

1H并且

2H5、

H

1H或者

2HHintikka引理：每一个命题hintikka集是可满足的。完备性：如果X是一个重言式，那么X有一个tableau证明过程。tableau推理举例((P→﹁Q)∧(﹁R→P)∧Q)=>R证明：先将((P→﹁Q)∧(﹁R→P)∧Q)∧﹁R化为合取范式

(﹁P∨﹁Q)∧(R∨P)∧Q∧﹁R(1)﹁P∨﹁Q(2)R∨P(3)Q(4)﹁R(5)RP(6)﹁P﹁Q***谓词逻辑:是命题逻辑的推广，命题逻辑是谓词逻辑的特殊情况。因为任何一个命题都可以通过引入具有相应含义的谓词（个体词视为常量）来表示，或认为命题是没有个体变元的零元谓词。函数：函数不单独使用，是嵌入在谓词中，用小写字母表示。

father(x):表示x的父亲；

P(x):表示x是教师；

P(father(x):表示x的父亲是教师。2一阶谓词逻辑量词:用来表示个体数量的词，对个体所加的限制、约束的词。符号：：全称量词，：存在量词。凡事物都是运动的。(x)(x是运动的）

(x)(P(x)):当且仅当对论域中的所有x来说，P(x)均为真时方为真，这就是全称量词的定义。当且仅当有一个x0D,使P(x0)=F时，(x)(P(x))=F。2一阶谓词逻辑（2）有一事物，它是动物。(

x)(x是动物）

(x)(Q(x)):当且仅当在论域中至少有一个x0，Q(x0)为真时方为真，这就是存在的定义。当且仅当所有xD,使Q(x)=F时，(

x)(Q(x))=F。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俱乐部，ALPINE俱乐部的成员不是滑雪运动员就是登山运动员。登山运动员不喜欢雨，而且任何不喜欢雪的人都不是滑雪运动员。Mike讨厌Tony所喜欢的一切东西，而喜欢Tony所讨厌的一切东西。Tony喜欢雨和雪。(1)定义谓词：Sportman(x,y)表示x是运动y的运动员Like(x,z)表示x喜欢z(2)i.ALPINE俱乐部的成员不是滑雪运动员就是登山运动员F1:Sportman(x,Snow)→Sportman(x,Mountain)ii.登山运动员不喜欢雨F2:Sportman(x,Mountain)→Like(x,Rain)iii.任何不喜欢雪的人都不是滑雪运动员F3:x[Like(x,Snow)]→Sportman(x,Snow)iV.Mike讨厌Tony所喜欢的一切东西，而喜欢Tony所讨厌的一切东西。Tony喜欢雨和雪。F4:Like(Mike,Rain)∧Like(Mike,Snow)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))}是可合一的，其合一为

={a/x,f(b)/y}2.3一阶谓词归结推理(1)假设有以下前提知识：

（1）自然数是大于零的整数；（2）所有整数不是偶数就是奇数；（3）偶数除以2是整数。求证：所有自然数不是奇数就是一半为整数的数。（1）定义谓词N(x)表示x是自然数；I(x)表示x是整数；E(x)表示x是偶数；O(x)表示x是奇数；GZ(x)表示x大于零；S(x)表示x除以2；（2）将前提条件及要求证的问题分别以谓词公式表示出来。F1:x(N(x)→GZ(x)∧I(x))F2:x(I(x)→E(x)∨O(x))F3:x(E(x)→I(S(x)))G:x(N(x)→(O(x)∨I(S(x))))（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))))(4)利用归结原理对上述子句进行归结推理⑧

I(t)∨E(t)③⑥归结，

={t/y}⑨

E(t)④⑦归结，

={t/z}⑩

I(t)⑧⑨归结⑾

N(t)②⑩归结⑿NIL⑤⑾归结2.3一阶谓词归结推理(2)用归结的方法回答问题：“有没有ALPINE俱乐部的一个成员，他是一个登山运动员但不是一个滑雪运动员？”F1:Sportman(x,Snow)→Sportman(x,Mountain)F2:Sportman(x,Mountain)→Like(x,Rain)F3:x[Like(x,Snow)]→Sportman(x,Snow)F4:Like(Mike,Rain)∧Like(Mike,Snow)G:x[Like(x,Snow)∧Like(x,Rain)]①Sportman(x,Snow)∨Sportman(x,Mountain)②Sportman(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)⑦Like(Mike,Snow)∨ANSWER(Mike)④⑥归结，

={Mike/x}⑧ANSWER(Mike)

⑤⑦归结2.3一阶谓词归结推理(3)下列刑侦知识①John是贼;②Paul喜欢酒(wine);③Paul也喜欢奶酪(cheese);④如果Paul喜欢某物则John也喜欢某物;⑤如果某人是贼,而且他喜欢某物,则他就可能会偷窃该物。求证：John可能会偷盗什么？(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(Paul,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)1、已知规则1：任何人的兄弟不是女性。规则2：任何人的姐妹必是女性。事实：Mary是Bill的姐妹。求证：用归结推理方法证明Mary不是Tom的兄弟。

规则1表示为xy(brother(x,y)woman(x))事实表示为sister(Mary,Bill)作业2、用归结法证明A1∧A2∧A3B，其中A1=(

x)((C(x)∧D(x))(y)(G(x,y)∧E(y)))A2=(x)(C(x)∧F(x)∧(

y)(G(x,y)F(y)))A3=(y)(D(x)∧F(x))B=(x)(E(x)∧F(x))2.3一阶谓词归结推理(5)3、证明子句集S={P∨Q,Q,P}是不可满足的。4、用反演归结证明定理，证明过程是这样结束的。若（），则定理得证.5、在命题逻辑下，可以归结的子句C1和C2，在某解释下C1和C2为真，则其归结式C在该解释下（）

A.必真B.必假C.不一定作业6、设两个子句：C1=P(x)∨Q(x)，C2=

P(a)∨T(z),在替换，其归结式为.7、设C1=P(a)∨Q(x)∨R(x),C2=P(y)∨Q(b)，求其二元归结式。设C1=P(x)∨Q(x),C2=Q(g(x))，求其二元归结式。

2.3一阶谓词归结推理(6)8、任何通过历史考试并中了彩票的人是快乐的。任何肯学习或幸运的人可以通过所有的考试，John不学习但很幸运，任何人只要是幸运的就能中彩。求证：John是快乐的作业9、某人被盗，派出所派出5个侦察员去调查。研究案情时，侦察员A说：“赵和钱至少有一个人作案”；侦察员B说：“钱和孙至少有一个人作案”；侦察员C说：“孙和李至少有一个人作案”；侦察员D说：“赵和孙至少有一个人与此案无关”；侦察员E说：“钱和李至少有一个人与此案无关”。如果这5个侦察员的话都可信的，试问谁是盗窃犯呢？2.4一阶谓词tableau推理(1)全称量词存在量词

(t)

(t)(x)Ф

(x)ФФ{x/t}

Ф{x/t}(x)Ф

(x)ФФ{x/t}

Ф{x/t}

(t)

(p)公式中的任意项t一个新的参数p一阶tableau扩展规则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)对于一个自由变量xf为一个Skolem化的函数,x1,…,xn是所有的tableau中的自由变量一阶tableau扩展规则﹁[(w)(

x)R(x,w,f(x,w))→(w)(

x)(y)R(x,w,y)](w)(

x)R(x,w,f(x,w))﹁(w)(

x)(y)R(x,w,y)(

x)R(x,a,f(x,a))﹁(

x)(y)R(x,v1,y)﹁(y)R(b(v1),v1,y)R(v2,a,f(v2,a))﹁R(b(v1),v1,v3)

={v1/a,v2/b(a),v3/f(b(a),a)}2.4一阶谓词tableau推理(4)含等词tableau自反规则:句子t≈t加到子句集S的tableau的任何一个分枝末尾产生另一个tableau．这里t是Lpar的任何项直观表示为：

t≈t替换规则

如果t≈u和Φ(t)产生在S的tableau分枝上，Φ(u)被加到tableau后，产生另一个tableau．这里t和u是Lpar的任何封闭项．t≈uΦ(t)Φ(u)2.5

tableau推理应用(1)数据库修正给定一个数据库实例r和一个完整性约束集合IC．对于IC和r的tableau，TP(IC∪r)是一个以公式集IC∪r为根节点的推理树，每个tableau分枝B为I∪r形式，I∈TP(IC)，I称为分枝的IC部分，如果r是不相容的，tableau是封闭的，即tableau存在封闭分枝．由于IC是相容的，因此一个tableau的IC部分永远是不封闭的，只有r和IC相结合才能产生一个封闭的tableau。考虑完整性约束:

x(P(x)→

yQ(x,y))和一个数据库实例r={P(a),Q(b,d)},a、b、c∈D，以TP(IK∪r)为根的tableau.

x(P(x)→

yQ(x,y))P(a),Q(b,d)P(a)→Q(a,f(a))¬P(a)Q(a,f(a))不相容的tableau**2.5

tableau推理应用(2)自然语言理解

Maryismarried.Shehasnohusband.

﹁(

x)h(Mary,x)：表示“Maryhasnohusband”w(Mary)：表示“Maryisawoman”

x(w(x)∧m(x)→(

y)h(x,y))：表示“everymarriedwomanhasahusband”

m(Mary)﹁(

x)h(Mary,x)

x(w(x)∧m(x)→(

y)h(x,y))w(Mary)﹁h(Mary,y)﹁(w(x)∧m(x))(

y)h(x,y)﹁w(o)﹁m(x)h(x,c1)⊥⊥2.5

tableau推理应用(3)电路仿真

+123输入12g1g2g3g4g5输出全加器电路图门电路及其类事实：xor_gate(g1).xor_gate(g2).and_gate(g3).and_gate(g4).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规则，只是对公式构造集进行扩展，使之更接近相应的逻辑系统。（2）引入相应的谓词，将二元关系的性质用逻辑公式来表示。

（1）将语义结构中的二元关系显式地表现出来。

1.引言1.1tableau实质1.2Tableau方法回顾序号时间提出者内容11955Beth提出tableau术语，目的是寻找一个反例21959Beth给出Gentzen的消除理论基于tableau的证明。31968Smullyan利用模型存在定理证明了tableau方法。41969Miglioli首次将tableau方法应用于直觉逻辑。51972Fitting首次将tableau方法应用于模态逻辑S4系统中。61974Surma首次将tableau方法应用于多值Łukasiewicz逻辑中。71986Bryant提出决策图tableau方法，能表达一个很大的可满足的公式模型。81991Fitting出版了《FirstorderlogicsandAutomatedTheoryProving》一书，将tableau方法带如空前繁荣阶段。91994Hahnle提出子句tableau方法，采用结构保留子句转换方法进行证明。102001Bertossi将tableau方法应用于数据库、自然语言理解、诊断、专家系统中。1.3研究的意义

人工智能研究的基础工作，许多重要的人工智能系统，都以推理系统为其核心部分。

对人工智能的其它分枝产生深远的影响，提出的推理方法已被应用于人工智能的各个领域。

专家系统问题解答系统学习系统程序的自动综合与合成医疗系统信息检索1.4研究现状含量词tableau改造技术

Fitting提出了循环控制

-规则应用次数h的技术。increate_prove(Fml，H):－prove（Fml，[]，[]，[]，H）

increate_prove(Fml，H):－NewHisH+1，H<=VarLim，

increate_prove（Fml，NewH）。(1)相关技术和策略的研究非相关部分剪枝技术由Oppacher提出的tableau压缩技术。

j

１

N……::封闭没用封闭BBtableau非相关部分剪枝技术

因子分解技术因子分解技术作为模型删除而引入。﹁p﹁qN3N2p﹁qq﹁pN1N4因子分解技术实现公式集{p∨q,p∨﹁q,﹁p∨q,﹁p∨﹁q}的证明过程1.4研究现状子句tableau方法超tableau方法决策图tableau方法翻译成整数规划的tableau方法(2)理论和方法的研究1.4研究现状直觉逻辑模态逻辑多值逻辑非单调逻辑

(3)非经典逻辑扩展的研究数据库修正完整性检查查询和变更数据库记录(1)数据库方面的应用1.5tableau应用1.5tableau应用

使用超tableau推理的观点来解决诊断问题。实现了基于tableau的诊断系统NIHIL(2)诊断方面的应用

利用tableau模型生成的算子RM有效地处理了自然语言知识积累的问题提出了PUHRtableau方法，有效地解决了含等词子句的自反和替换带来的不封闭问题实现了基于tableau的RM算子及扩展问题的系统——HOU(3)自然语言理解方面的应用1.5tableau应用1.6

主要工作⑴在

-规则基础上，提出对

＋-规则改进的

＋＋-规则，结果表明，改进后的系统对

-公式在推理空间效率上有较大的提高。在

-规则基础上给出识别

-公式方法，提出了含

-公式的tableau推理的改进策略，

-公式不再需要实例化，缩短了tableau的证明过程。

主要工作⑵在多值逻辑tableau方法研究方面，提出布尔剪枝方法，将带符号的公式与集合的上集／下集联系起来，使含量词的一阶多值逻辑公式的扩展规则大大简化。并将经典逻辑中的结构保留子句转换方法应用到带符号的多值逻辑公式中，产生输入规模是线性的范式。引入极性的概念，减少冗余子句的产生。

⑶在增添扩展规则的tableau方法的基础上提出了一种新的含等词tableau方法——等式合一方法。将tableau分成两个阶段，等词单独处理，通过提取等式合一问题并求解解替换封闭tableau，进一步限制了tableau的搜索空间，提高了tableau的推理效率。

主要工作主要工作⑷使用SWI-PROLOG语言在微机上设计实现了基于tableau的定理证明系统TableauTAP，并证明了其正确性。该系统可以证明不含等词的经典逻辑公式和多值逻辑公式，通过预处理自动生成tableau规则，因此容易对其功能进行扩展。令{A1,A2,…,An}为公式的有限集合。⑴

下列分枝树为公式{A1,A2,…,An}的一个tableau:A1A2

An⑵如果T为{A1,A2,…,An}的一个tableau，且T′为T应用tableau推理规则后的结果，那么T′也是{A1,A2,…,An}的一个tableau。1.7tableau定义：

1

1…

n

:

n

1(y)

1(f(x1,…,xn))

y是一个自由变量

f是一个新的Skolem函数符号，

x1,…,xn是分枝中出现的自由变量-规则-规则-规则-规则推理规则：（1）研究现状（2）问题提出（3）本文工作（4）实验对比2、逻辑基础f(x1)/x2a/x1⑴

(

x)(((

z)P(z))∨

P(x))⑵

(((

z)P(z))∨

P(x1))⑶

(

z)P(z)⑷

P(x1)⑸

P(x1)⑹

P(a)＊

21⑴

(

x)(((

z)P(z))∨

P(x))⑵

(((

z)P(z))∨

P(x1))⑶

(

z)P(z)⑷

P(x1)⑸

P(x1)⑹

P(f(x1))⑺

(((

z)P(z))∨

P(x2))⑻

(

z)P(z)⑼

P(x2)⑽

P(x2)

＊Fitting方法Hahnle的

+方法例：证明公式(

x)(((

z)P(z))∨

P(x))是恒真的。

1(f(x1,…,xn)

f是一个新的Skolem函数符号，

x1,…,xn是分枝中出现的自由变量

(f(x1,…,xn)

f是一个新的Skolem函数符号，

x1,…,xn是出现在

中的自由变量．

1(x)

-规则

+-规则

+-规则与

-规则的区别是：在

-规则x1,…,xn是指出现在分枝中的自由变量，在

+-规则x1,…,xn指是出现在

中的自由变量．用

+-规则代替

-规则产生的tableau证明的长度呈幂指数的减少。（1）研究现状

-规则要求被Skolem化的函数符号是新的，且函数中包含分枝中出现的所有自由变量．显然，由于

-规则的不确定性以及

-规则的限制，可使一个简单的证明变得很复杂，延迟了tableau的封闭时间。由于

-规则替换的任意性，可导致在同一tableau证明中，

-规则被多次使用，使得tableau结构中出现多个自由变量。(2)问题提出例：应用

-、

+-、

+＋-规则证明公式集{(

x)

P(x),(

x)P(x)∨(

y)P(y)}是不可满足的。⑵

(

x)P(x)∨(

y)P(y)⑺

P(g(x1))⑴

(

x)

P(x)⑶

P(x1)⑷

(

x)P(x)⑸(

y)P(y)⑹

P(f(x1))⑻

P(x2)⑼

P(x3)f(x1)/x2g(x1)/x3**应用

－规则⑸(

y)P(y)⑼

P(x3)⑴

(

x)

P(x)⑵

(

x)P(x)∨(

y)P(y)⑶

P(x1)⑷

(

x)P(x)⑹

P(c1)⑻

P(x2)c1/x2c2/x3**应用

+－规则⑺

P(c2)⑴

(

x)

P(x)⑶

P(x1)⑷

(

x)P(x)⑸(

y)P(y)⑹

P(c)c/x1**⑵

(

x)P(x)∨(

y)P(y)应用

++－规则

+＋－规则为：

(f[

](x1,…,xn)f[

]是赋予的函数符号，在等价类[

]中所有公式赋予唯一的函数符号f[

]

Σ。(3)本文工作

对于

-公式，通过skolem否定范式转换后的公式中不再存在。因此对于

-公式的改进，需要在否定范式的转换谓词change_nnf中考虑。LeanTAP系统TableauTAP系统

SWI-Prolog语言change_nnf(ex(X,Fml)，FreeV,NNF,Paths):-!，copy_term((X,Fml,FreeV)，(Fml,Fml1,FreeV))，copy_term((X,Fml,FreeV)，(a,Fml2,FreeV))，nnf(Fml1，FreeV，NNF，Paths)。（4）系统的实现及实验对比问题序号

-规则

+-规则

++-规则节点数(个)时间(毫秒)节点数(个)时间(毫秒)节点数(个)时间(毫秒)1301403014018852411683615036150326872687268747520175201531605180304892106015464917034130341307104280104280581708331503315020100927135271352713510872098720946140

实验结果

可以看出，从tableau扩展节点数和封闭时间上进行了比较，其中有2个问题，应用

+、

++规则没有变化，其中有6个问题，应用

++规则后，节点数和时间上都有较大幅度的减少。3、语义tableau中γ-规则的改进(1)研究现状(2)问题提出(3)本文的工作(4)实验对比

如果一个tableau分枝B包含一个公式P(x)，在tableau过程中，x必然出现在某些分枝上，为了封闭这些分枝需要多次对x进行实例化(

P(a)∨

P(b))∧((

x)P(x))

P(a)∨

P(b)(

x)P(x)P(y)

P(a)

P(b)P(a)a/yP(b)b/y(1)研究现状

在tableau证明中,

-公式对其中包含的自由变量需要进行多次不同的实例化。典型的例子是群论中的结合律(

x)(

y)(

z)((x·y)·z

x·(y·z))，应用该定律即使证明一个非常简单的定理，也要对其中的x、y、z进行多次不同的实例化替换。

(2)问题提出在tableau实现时，对

-规则应用次数的限制致关重要:限制的次数太少，不能满足推理需要的实例，使一个恒真的公式得不到tableau证明。限制的次数过多，由于

-规则使用次数的不确定性，必然会导致大量的冗余推理产生，使证明过程的搜索空间膨胀。

令Γ为理论，φ为tableauT的一个分枝B上的公式，对于变量x,通过向T的分枝B中增加(

x)φ而得到tableauT’,如果T╞ΓT’,那么对于x，在B上公式φ是γ-公式。⑴

用

-规则，x是引入的自由变量；或⑵

关于x的全称公式ψ应用

-，

-，

-规则。R是识别

-公式的方法，这里R(B,F)包含变量x，公式φ被加入到B中，通过（3）本文的工作含γ-公式的tableau

一个公式G(x)被识别为关于x的

-公式，那么G(x′)、G(x″)、…能被加入到分枝中，而不影响其它分枝或产生新分枝。一旦一个公式被识为

-公式，那么寻找一个封闭tableau的替换

就变得比较容易：对于

-公式中的变量不需要实例化。

令R为识别

-公式的方法，带分枝B1,…,Bk的自由变量tableauT是封闭的，当且仅当存在替换σ1,…,σk使得：⑴对于1≤i≤k，公式Fi,¬Gi∈Bi,并且Fiσi＝Giσi。⑵只有变量x对于公式Fi,Gi∈BiFj,Gj∈Bj是

-公式时，存在替换σi和σj(1≤i≤j≤k)有xσi≠xσj。(

P(a)∨

P(b))∧((

x)P(x))

P(a)∨

P(b)

(

x)P(x)

P(y)

P(a)

P(b)

P(y)被识别为

-公式，因此P(y)不再需要实例化，可立即封闭。这样会使tableau过程缩短，搜索空间减小。例：{(

x)((g(x)≈f(x))∨

(x≈a))，(

x)(g(f(x))≈x)，b≈c，P(g(g(a)),b)，

P(a,c)}

⑴(

x)((g(x)≈f(x))∨

(x≈a))⑵(

x)(g(f(x))≈x)⑶b≈c⑷P(g(g(a)),b)⑸

P(a,c)⑹g(f(x1))≈x1⑺(g(x2)≈f(x2))∨

(x2≈a)

⑻(g(x2)≈f(x2)⑼

(x2≈a)⑽P(g(f(a)),b)＊⑾

P(a,b)⑿P(a,c)＊如果等式⑻应用到⑷的过程中，

{g(a)/x2}代替

{a/x2}将产生错误的方法，即

⑽*

P(f(g(a)),b)代替

⑽P(g(f(a)),b)那么tableau不能封闭。tableau在替换{a/x1，a/x2}下是封闭的．因此Fitting方法也存在着不确定性问题，随着tableau推进顺序的不同，可导致不同的结果。该方法很难用于机器实现，并且不可避免地产生回溯。利用的识别

-公式的方法，等式⑹被识别为关于x1的

-公式，因此x1不再需要实例化，例子的tableau过程中的⑽⑾⑿可以删除，通过替换{a/x2}即可封闭。

用VisualProlog语言在Windows环境下进行了系统UniTAP的实现，程序中将识别出的

-变量保存在一个表中，可以对表中的变量进行实例化，使分枝中的实例互不影响。使用的谓词如下：

(4)实验对比Prove（

Fml，UnExp，Lits，DisV，FreeV，UnivV，VarLim）自由变量被实例化的最大次数

出在Fml中的全称变量表出现在目前分枝中的自由变量表

除

变量以外的所有Prolog项出现在目前分枝中的文字表

扩展过程中的公式待扩展的源公式

利用LeanTAP系统和UniTAP系统处理Pelletier问题的实验结果Pelletier问题序号VarLim限定次数LeanTAP系统UniTAP系统封闭分枝数运行时间(msec)封闭分枝数运行时间(msec)171142201013218219018519243302202206318017621284626304222730742902314243421024633608202092535409333226316563122382748686843328354012374292116096501302427622333135834346532310487637733111218511034526710981124303541149112036633513302

-公式不再需要实例化，大大缩短了tableau的证明过程，减少封闭分枝，提高了推理效率。另外在非经典逻辑中的识别

-公式的方法与经典逻辑类似，因此只要稍加修改就可将该方法扩展到非经典逻辑中。

含等词的tableau方法研究现状问题提出本文工作实例对比分析小结4、利用等式合一处理含等词tableauJeffrey方法（1）含等词的tableau方法分析t≈s

s≈t

[t]

[t]

[s]

[s]

Jeffrey含等词扩展规则

存在问题无关公式的数目随着谓词元数的增加呈幂指数增长扩展规则是对称的，它的应用不受限制。这就导致了在推理过程中，产生大量的无关公式Reeves方法（1）含等词的tableau方法分析P(s1,…,sn)

P(t1,…,tn)

(s1≈t1)

…

(sn≈tn)

(s1≈t1)

…

(sn≈tn)

Reeves含等词扩展规则

f(s1,…,sn)≈f(t1,…,tn)优点：对封闭分枝的搜索更直接存在问题：如果一个分枝包含几个等式和不等式，新的扩展规则也可能被看成同样的等式和不等式来扩展，这样连续不断的新的扩展分枝被加入到tableau中。分枝的增长随着在分枝中等式的数目的增加，呈幂指数的增长，因此Reeves方法不利于机器实现。Fitting方法（1）含等词的tableau方法分析t≈s

s≈t

[t´]

[t´]

(

[s])μ(

[s])μ

含等词自由变量tableau扩展规则μ是t和t´的MGU，μ应用到整个tableau

存在问题：存在着不确定性问题,随着tableau推进顺序的不同，可导致不同的结果很难用于机器实现，并且不可避免地进行回溯

在增添扩展规则的tableau方法的基础上提出一种新的含等词tableau算法——等式合一方法。在该方法中，将tableau分成两个阶段，等词单独处理，通过提取等式合一问题并求解解替换封闭tableau，该方法进一步限制了tableau的搜索空间，提高了tableau的推理效率。（2）问题提出

等式合一问题<E，s，t>包含形如(

x1)…(

xn)(l≈r)的等式的有穷集合E、项s和t。一个替换

为等式合一问题的解当且仅当E

╞(s

≈t

)成立。等式合一(3)本文工作

令B为一个tableau分枝，等式合一问题集合包含集合序对<E(B)，P(B)>，其中:⑴集合E(B)定义为：{s≈t：s≈t∈B}

E(B)；⑶对于B上的每个不等式

(s≈t),{s

,t

)}

P(B)。⑵对于B上的潜在封闭原子对p(s1,…,sn)和

p(t1,…,tn)(这里p≠≈)，存在某一替换，

使得{s1

≠t1

∨…∨sn

≠tn

}

P(B)；等式合一问题集合分阶段tableau

将tableau扩展分成两个阶段。第一阶段是在处理等词之前，应用tableau扩展规则，将所有的tableau扩展完成，在这个过程中要求对

-规则应用次数进行限制。第二阶段是处理等词，通过适当的手段，限制等词的使用，以避免无关公式的产生。

分阶段tableau方法不需要在等词应用规则和其它扩展规则之间转换，因此在第一阶段完成以后，许多公式不再需要。从第二阶段开始只需要考虑等式、不等式以及潜在的封闭原子对，这样使含等词的tableau在一个更适合的数据结构P(B)和E(B)下进行。基本思想：完备性：如果公式

是不可满足的，q足够大，那么T是T2封闭的。可靠性：如果T是T2封闭的，那么公式

是不可满足的。T是关于公式

的tableau，q是

-规则应用的限定次数，利用等式合一解替换封闭tableauTableauT是T2封闭的，当存在一个基替换

，对于T上的每一个分枝B，存在一个析取（t1≠s1∨…∨tn≠sn）∈P(B)使得1≤i≤n，[ti

]B=[si

]B.定义定理begin<t>={tid}n=1whilen<=Ndobegin

将<t>

中不被另一元素包含的所有元素加入到Θn中

s

=H(<t>)whileflagdobegin

s

加入到集合Θn中

是s和等式G∈E(B)一端的MGU

if

存在thenflag=trueelseflag=false

n=n+1endendend算法(计算集合<t>的等价序列的近似算法)输入：项t、等式集合E(B)、n的最高次数输出：项t的等价序列集合<t>等式合一问题的实现算法（4）实例对比分析(

x)[g(f(x))≈c∧(f(x)≈g(x)∨

)]→g(g(a))≈g(f(b))为重言式．其中

为不可满足的任意公式．tableau第一阶段的扩展如下：

F(

x)[g(f(x))≈c∧(f(x)≈g(x)∨

)]→g(g(a))≈g(f(b))√T(

x)[g(f(x))≈c∧(f(x)≈g(x)∨

)]√Fg(g(a))≈g(f(b))Tg(f(x))≈c∧(f(x)≈g(x)∨

)√Tg(f(x))≈cTf(x)≈g(x)∨

√

Tf(x)≈g(x)T

*

后面标注“√”的为不再使用的公式，第一阶段完成后，tableau扩展已经完成，但tableau没有封闭。

例：证明公式设未封闭分枝为B，B转换成集合E(B)和P(B)。

E(B)={g(f(x))≈c,f(x)≈g(x)}P(B)={g(g(a))≠g(f(b))}Tableau的第二阶段转换成计算<g(g(a))>和<g(f(b))>的合一元素。①g(f(x))≈c②f(x)≈g(x)g(g(a))g(f(b))①g(f(x))≈c②f(x)≈g(x)g(g(a))g(f(b))f(g(a)){g(a)/x}g(f(a)){a/x}P(B)E(B)第一步第二步①g(f(x))≈c②f(x)≈g(x)g(g(a))g(f(b))f(g(a)){g(a)/x}f(f(b)){f(b)/x}g(f(a)){a/x}g(g(b)){b/x}cid①g(f(x))≈c②f(x)≈g(x)g(g(a))g(f(b))f(g(a)){g(a)/x}f(f(b)){f(b)/x}g(f(a)){a/x}g(g(b)){b/x}c{a/x}cid第三步第四步

（1）如果使用Fitting方法证明同一公式为重言式，

-公式的使用次数必须提高。（2）在同一启发搜索算法下，证明不等式g(g(a))≠g(f(b))的不可满足性，将产生15个中间等式，并需要几次的自由变量替换。（3）如果使用Jeffrey方法证明同一公式为重言式，等式规则的应用次数依赖于使用等式的次序，最好的情况下只需要2个分枝即封闭，然而在较差的情况下可以产生几百个分枝。

提出利用等式合一处理含等词tableau方法，将tableau扩展分成两个阶段。第一阶段是在处理等词之前，应用tableau扩展规则，将所有的tableau扩展完成，在这个过程中要求对

规则应用次数进行限制。第二阶段是处理等词，通过提取等式合一问题并求解解替换封闭tableau，在启发式的帮助下计算等价类的方法，限制等词的使用，以避免无关公式的产生，在效率和实现上都有较大的提高。

（5）小结

一是二是将计算等价类的结果以树的结构进行存储，利用树的特点，进行搜索的优化，提高推理效率。改进启发式算法，提高计算等价类的速度。5、多值逻辑语义tableau方法(1)含量词的一阶多值逻辑Tableau(2)问题提出(3)利用布尔集格对tableau方法的改进(4)含广义量词的四值逻辑tableau实例(5)实例分析(6)多值逻辑正则公式的tableau方法(7)小结

(Q(

))-1(S)={I

I

N，Q(

)(I)

S}(Q(

))-1({0})={{0},{0,},{0,1},{0,,1}}(1)含量词的一阶多值逻辑Tableau2121扩展规则：符号引入：

含量词的tableau方法是由Carnielli（1987）引入，后来由Zabel(1993)在理论上找到了可满足的扩展规则，并给出了可靠性和完备性的证明。然而对于自动定理证明来说，其实现难度非常大，为此找出一种扩展分枝更少的有效推理方法。提出了布尔剪枝方法，将带符号的公式与集合的上集／下集联系起来，使含量词的一阶公式的扩展规则大大简化。通过对布尔剪枝方法的进一步探讨，建立了一类特殊一阶多值逻辑正则公式的更为简捷的tableau推理方法，该方法使得含量词的一阶多值逻辑tableau推理类同于经典逻辑tableau方法。(2)问题提出在多值逻辑中例：在一阶三值Kleene逻辑中，可以对{0}(

x)

(x)进行扩展，其中(Q(

))-1({0})={{0},{0,

},{0,1},{0,,1}}。扩展结果如下：{0}

(c)

{0}

(t1)

{0}

(c){}

(d)

{0,}

(t2)

{0}

(c){}

(d){1}

(e){0,,1}

(t3)

{0}

(c)

{1}

(e){0,1}

(t4)

含量词的一阶多值逻辑Tableau212121212121{0}(

x)

(x)

定义F，

F

N，产生的关于布尔集格2N的集合的上集为U(F)={X

X

N,X∩F

}。定义I，

I

N，产生的关于布尔集格2N的集合的下集为D(I)={X

X

N,

X

I}。（3）利用布尔集格对tableau方法的改进⑴如果(Q(

))-1(S)=U(F)，则S(

x)

(x)是可满足的当且仅当对于新的Skolem常数c，F

(c)是可满足的。⑵如果(Q(

))-1(S)=D(I)，则S(

x)

(x)是可满足的当且仅当对于所有的基项t，I

(t)是可满足的。

设N为有穷真值集，S

N，定理定义例子中，一阶三值Kleene逻辑中，

因为(Q(

))-1({0})=U({0})={{0},{0,},{0,1},{0,,1}}，因此规则可简化为：

{0}(

x)

(x){0}

(c)

另外，因为(Q(

))-1({0})=D({0})={{0}}，因此规则

{0}(

x)

(x){0}

(t)是成立的。这一结论也是与经典情况一致的。2121

将含量词的tableau方法与布尔集格相结合，简化了tableau的扩展分枝，在本章中我们称之为布尔剪枝。在效率和实现上都有较大的提高时间效率空间效率Zabel方法O(nk)O(n*k)布尔剪枝方法O(n*k)O(n)例：考虑真值集合FOUR={⊥,f,t,⊤}，定义量词Π，Q(Π)=，这里

为格中的交操作。⊥ft{⊥,f}{}{⊥}{f}{t}{⊤}{⊥,t}{f,t}{⊥,⊤}{f,⊤}{t,⊤}{⊥,f,t}{⊥,f,⊤}{⊥,t,⊤}{f,t,⊤}FOUR四值布尔集格四值逻辑格结构（4）含广义量词的四值逻辑tableau实例⊤

以{⊥}为例，tableau扩展结果如下：{⊥}

(c){⊥}

(c){⊥}

(c){f}

(c){⊥}

(c){⊥}

(c){⊥}

(c){⊥}

(c){f}

(c){⊥}

(c){f}

(d){t}

(d){t}

(d){⊤}

(d){f}

(d){f}

(d){t}

(d){t}

(d){f}

(d){t}

(e){⊤}

(e){⊤}

(e){⊤}

(e){t}

(e){⊤}

(f){⊥}(Πx)

(x)Q(Π)=⊓

Q(Σ)=⊔

设L=<N,⊓,⊔>为真值有穷集合N上的格，定义分布量词Π和Σ如下：则有下列式子成立：定理⑴如果i∈MI(L)，那么(Q－１(Π))({i})=U({i})∩(D(

i)∪{

})。⑵如果L是分配格并且i∈MI(L)，那么(Q－１(Π))(

i)=U(

i)。⑶对于任何i∈N和分配格L:(Q－１(Π))({i})=(U(

m))∩(D(

i)∪{

})，其中Mi是MI(L)∩

i中的最小元素。⑷对于任何i∈N和分配格L:(Q－１(Π))(

i)=U(

m)，其中Mi是MI(L)∩

i中的最小元素。⑸对于任何i∈N：(Q－１(Π))(

i)=D(

i)。⑹如果i∈JI(L)，那么(Q－１(Σ))({i})=U({i})∩(D(

i)∪{

})。⑺如果L是分配格并且i∈JI(L)，那么(Q－１(Σ))(

i)=U(

i)。⑻对于任何i∈N和分配格L:(Q－１(Σ))({i}