人工智能117

自动定理证明AutomatedTheoremProving计算机科学与技术学院软件形式化与自动推理学科组2010年10月1、自动定理证明理论及方法2、基于tableau的自动定理证明自动定理证明理论及方法1、命题逻辑自动定理证明方法2、一阶谓词逻辑自动定理证明方法古典数理逻辑命题逻辑:一句有真假意义的话。(真值:T和F)是谓词逻辑的一种简单情形。简单命题（原子命题）：不包含联结词的命题。复合命题：两个或几个简单命题用联结词联结构成的命题。谓词逻辑:1命题逻辑1.1命题联结词及真值表PPFTTF否定：PQP∨QFFFFTTTFTTTT析取：PQP∧QFFFFTFTFFTTT合取：FTFTFTTFFTTTPQPQ蕴涵：FTFFFTTFFTTTPQPQ等价：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，生成一个tableauT*．下面证明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、对于任何命题字母AH,不同时存在﹁AH．2、FH;﹁TH;3、﹁﹁ZHZH;4、H1H并且2H5、H1H或者2HHintikka引理：每一个命题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)均为真时方为真，这就是全称量词的定义。当且仅当有一个x0D,使P(x0)=F时，(x)(P(x))=F。2一阶谓词逻辑（2）有一事物，它是动物。(x)(x是动物）(x)(Q(x)):当且仅当在论域中至少有一个x0，Q(x0)为真时方为真，这就是存在的定义。当且仅当所有xD,使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,Sno