自動(dòng)定理證明

AutomatedTheoremProving1、自動(dòng)定理證明理論及方法2、基于tableau的自動(dòng)定理證明自動(dòng)定理證明理論及方法1、命題邏輯自動(dòng)定理證明方法2、一階謂詞邏輯自動(dòng)定理證明方法古典數(shù)理邏輯命題邏輯:一句有真假意義的話。(真值:T和F)

是謂詞邏輯的一種簡(jiǎn)單情形。

簡(jiǎn)單命題（原子命題）：不包含聯(lián)結(jié)詞的命題。

復(fù)合命題：兩個(gè)或幾個(gè)簡(jiǎn)單命題用聯(lián)結(jié)詞聯(lián)結(jié)構(gòu)成的命題。謂詞邏輯:1命題邏輯1.1命題聯(lián)結(jié)詞及真值表P

PFTTF否定：PQP∨QFFFFTTTFTTTT析?。篜QP∧QFFFFTFTFFTTT合?。篎TFTFTTFFTTTPQPQ蘊(yùn)涵：FTFFFTTFFTTTPQPQ等價(jià)：1.1命題聯(lián)結(jié)詞及真值表合式公式：命題演算的合式公式，規(guī)定為：（1）單個(gè)命題變?cè)旧硎且粋€(gè)合式公式；（2）如果A是合式公式，那么﹁A也是合式公式；（3）如果A，B是合式公式，那么A∧B,A∨B，A→B，A

B都是合式公式；（4）iff能夠有限次應(yīng)用(1)、(2)、(3)所得到的包含命題變?cè)?、?lián)結(jié)詞和括號(hào)的符號(hào)串是合式公式。定義1.2重言式重言式（永真式）：如果一個(gè)公式，對(duì)它的任一解釋I下其真值都為真。

P∨﹁P定義

一個(gè)公式，如有某個(gè)解釋I0，在I0下給公式真值為真，則稱(chēng)這公式是可滿足的。重言式是可滿足的。矛盾式是不可滿足的。1.2重言式重言式、矛盾式和不可滿足的公式關(guān)系：

公式A永真，當(dāng)且僅當(dāng)﹁A永假；

公式A可滿足，當(dāng)且僅當(dāng)﹁A非永真；

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

一些推理問(wèn)題的描述,常以自然語(yǔ)句來(lái)表示:

把自然語(yǔ)言形式化成邏輯語(yǔ)言,即以符號(hào)表示的邏輯公式；

根據(jù)邏輯演算規(guī)律進(jìn)行推理演算。

實(shí)例：如果我學(xué)習(xí)，那么我數(shù)學(xué)不會(huì)不及格；如果我不熱衷于玩撲克，那么我將學(xué)習(xí)；但我數(shù)學(xué)不及格。結(jié)論：我熱衷于玩撲克。解：設(shè)P:我學(xué)習(xí)Q:我數(shù)學(xué)不及格R:我熱衷于玩撲克

((P→﹁Q)∧(﹁R→P)∧Q)=>R歸結(jié)法是定理機(jī)器證明的重要方法；是僅有一條歸結(jié)推理規(guī)則的機(jī)械推理法；從而易于程序?qū)崿F(xiàn)；可推廣到謂詞邏輯的推理。1.4歸結(jié)推理法歸結(jié)證明過(guò)程1、證明A→B（定理）是重言式，等價(jià)于證A∧﹁B是矛盾式。使用歸結(jié)法就是從A∧﹁B出發(fā)。2、建立子句集S

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

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

P∨R)

形式，子句集合為：

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

P∨R)}3、對(duì)S作歸結(jié)對(duì)S的子句作歸結(jié)（消互補(bǔ)對(duì)），如子句P∨R

與﹁P∨﹁Q

作歸結(jié)，得歸結(jié)式R∨﹁Q

,并將這一歸結(jié)式放入S中，重復(fù)這過(guò)程。4、直到歸結(jié)出矛盾式□。歸結(jié)式的定義設(shè)C1=L∨C1’，C2=﹁L∨C2’為兩個(gè)子句，有互補(bǔ)對(duì)L和﹁L，則新子句:

R(C1,C2)=C1’∨C2’稱(chēng)作C1,C2的歸結(jié)式。歸結(jié)推理規(guī)則歸結(jié)過(guò)程就是對(duì)S的子句求歸結(jié)式的過(guò)程：C1∧C2=>R(C1,C2),R(C1,C2)是子句C1,C2的邏輯推論。

從而歸結(jié)是正確的推理規(guī)則。

設(shè)在任一解釋下，C1和C2均為真。若在這解釋下，L為真，則﹁L為假，從而必有C2’為真。于是在解釋下R(C1,C2)為真。若在這解釋下，﹁L為真，則L為假，從而必有C1’為真。于是在解釋下R(C1,C2)為真。因此，證明了C1∧C2=>R(C1,C2)。歸結(jié)推理舉例((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}歸結(jié)過(guò)程：(1)﹁P∨﹁Q(2)R∨P(3)Q(4)﹁R(5)﹁P(1)(3)歸結(jié)(6)

P(2)(4)歸結(jié)

(7)□(5)(6)歸結(jié)1.5tableau推理法（1）tableau定義令{A1,…,An}為一命題公式的有限集合：1、下列分支為{A1,…,An}的一個(gè)tableauA1

…

An2、如果T是一個(gè){A1,…,An}的tableau，對(duì)T應(yīng)用tableau擴(kuò)展規(guī)則生成T*，那么T*仍然是一個(gè)tableau。Tableau擴(kuò)展規(guī)則﹁

﹁ZZ﹁TFT﹁F

1

2

1

2Tableau有效性定義：一個(gè)命題公式集S是可滿足的，如果某一布爾值映射到S的每個(gè)成員都為T(mén).一個(gè)tableau分支是可滿足的，如果在個(gè)上面的命題公式集是可滿足的。一個(gè)tableauT是可滿足的，如果至少T上的一個(gè)分支是可滿足的。命題：如果任何tableau擴(kuò)展規(guī)則被應(yīng)用到可滿足的tableau，其結(jié)果為另一個(gè)可滿足的tableau．

證明．假設(shè)T是一個(gè)可滿足的tableau，對(duì)于T的分枝θ應(yīng)用表擴(kuò)展規(guī)則產(chǎn)生X，生成一個(gè)tableau

T*．下面證明T*也是可以滿足的．因?yàn)門(mén)是可以滿足的，T至少有一個(gè)可滿足的分枝，選擇這一分枝，記為τ．1)τ≠θ．規(guī)則應(yīng)用到θ上，τ仍為T(mén)*的分枝，因此T*是可以滿足的。2)τ=θ．θ本身是可滿足的，布爾賦值ν將θ中的所有公式映射為t．2a)X=α．那么θ被擴(kuò)展為α1和α2而產(chǎn)生T*．由于α產(chǎn)生在θ上，有ν(α)=t，ν(α)＝ν(α1)∧ν(α2)，因此ν必將ν(α1)和ν(α2)都映射為t．這樣ν將在Ｔ*的θ擴(kuò)展的每個(gè)公式都映射為t，因此T*是可以滿足的．2b)X=β．那么將左右兒子加到θ的最后節(jié)點(diǎn)上，標(biāo)記為β1和β2，而產(chǎn)生T*，由于β產(chǎn)生在θ上，ν(β)=t，但ν(β)＝ν(β１)∨ν(β２)，ν將β１或β2映射為t，ν將左側(cè)或右側(cè)的擴(kuò)展分枝映射為t．只要存在其一，T*就有可滿足的分枝，因此T*是可以滿足的．其它情況：X是﹁﹁Z，﹁ㄒ或﹁⊥，易證T*是可以滿足的．

命題：如果公式集S存在一個(gè)tableau，那么S是不可滿足的．證明．假設(shè)公式集S存在一個(gè)tableau，S是可滿足的．對(duì)S構(gòu)造一個(gè)開(kāi)始于S封閉的tableau，由于S是可滿足的，那么初始標(biāo)記為S的tableau是可滿足的，根據(jù)引理，S的tableau的每個(gè)子tableau都是可滿足的，包括最后封閉的tableau，這顯然是矛盾的，因此，S是不可滿足的．

命題tableau的有效性定理：如果X有一個(gè)tableau證明，那么X是重言式．證明．

假設(shè)X有一個(gè)tableau證明但是無(wú)效的．我們推出矛盾．由于X是無(wú)效的，因此有一個(gè)模型使得﹁X為真，對(duì)X的tableau證明開(kāi)始與標(biāo)有﹁X的一個(gè)分枝，并且是可滿足的tableau．由引理2可知，每個(gè)后繼tableau都是可滿足的，包括最后的封閉的tableau．但封閉的tableau不能是可滿足的．因此推出矛盾．所以如果X有一個(gè)tableau證明，那么X是有效的．1.5tableau推理法（2）命題hintikka集定義一個(gè)命題公式集合H稱(chēng)為Hintikka集，如果：1、對(duì)于任何命題字母AH,不同時(shí)存在﹁AH．2、FH;﹁TH;3、﹁﹁ZHZH;4、

H

1H并且

2H5、

H

1H或者

2HHintikka引理：每一個(gè)命題hintikka集是可滿足的。完備性：如果X是一個(gè)重言式，那么X有一個(gè)tableau證明過(guò)程。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***謂詞邏輯:是命題邏輯的推廣，命題邏輯是謂詞邏輯的特殊情況。因?yàn)槿魏我粋€(gè)命題都可以通過(guò)引入具有相應(yīng)含義的謂詞（個(gè)體詞視為常量）來(lái)表示，或認(rèn)為命題是沒(méi)有個(gè)體變?cè)牧阍^詞。函數(shù)：函數(shù)不單獨(dú)使用，是嵌入在謂詞中，用小寫(xiě)字母表示。

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

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

P(father(x):表示x的父親是教師。2一階謂詞邏輯量詞:用來(lái)表示個(gè)體數(shù)量的詞，對(duì)個(gè)體所加的限制、約束的詞。符號(hào)：：全稱(chēng)量詞，：存在量詞。凡事物都是運(yùn)動(dòng)的。(x)(x是運(yùn)動(dòng)的）

(x)(P(x)):當(dāng)且僅當(dāng)對(duì)論域中的所有x來(lái)說(shuō)，P(x)均為真時(shí)方為真，這就是全稱(chēng)量詞的定義。當(dāng)且僅當(dāng)有一個(gè)x0D,使P(x0)=F時(shí)，(x)(P(x))=F。2一階謂詞邏輯（2）有一事物，它是動(dòng)物。(

x)(x是動(dòng)物）

(x)(Q(x)):當(dāng)且僅當(dāng)在論域中至少有一個(gè)x0，Q(x0)為真時(shí)方為真，這就是存在的定義。當(dāng)且僅當(dāng)所有xD,使Q(x)=F時(shí)，(

x)(Q(x))=F。2.1自然語(yǔ)言的形式化1、所有的有理數(shù)都是實(shí)數(shù)。(x)(P(x)→Q(x))2、函數(shù)f(x)在[a,b]上的點(diǎn)x0處連續(xù)。()(>0→()(>0∧(x)(|x-x0|<→|f(x)-f(x0)|<)))3、設(shè)Tony、Mike和John屬于ALPINE俱樂(lè)部，ALPINE俱樂(lè)部的成員不是滑雪運(yùn)動(dòng)員就是登山運(yùn)動(dòng)員。登山運(yùn)動(dòng)員不喜歡雨，而且任何不喜歡雪的人都不是滑雪運(yùn)動(dòng)員。Mike討厭Tony所喜歡的一切東西，而喜歡Tony所討厭的一切東西。Tony喜歡雨和雪。(1)定義謂詞：Sportman(x,y)表示x是運(yùn)動(dòng)y的運(yùn)動(dòng)員Like(x,z)表示x喜歡z(2)i.ALPINE俱樂(lè)部的成員不是滑雪運(yùn)動(dòng)員就是登山運(yùn)動(dòng)員F1:Sportman(x,Snow)→Sportman(x,Mountain)ii.登山運(yùn)動(dòng)員不喜歡雨F2:Sportman(x,Mountain)→Like(x,Rain)iii.任何不喜歡雪的人都不是滑雪運(yùn)動(dòng)員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}的一個(gè)有限集合，其中vi是變量符號(hào)，ti是不同于vi的項(xiàng)，并且在此集合中沒(méi)有在斜線符號(hào)后面有相同變量符號(hào)的兩個(gè)元素。稱(chēng)ti為替換的分子，vi為替換的分母。合一：替換稱(chēng)為表達(dá)式集合{E1,…,Ek}的合一，當(dāng)且僅當(dāng)E1

=E2

=…=Ek

。表達(dá)式集合{E1,…,Ek}稱(chēng)可合一的，如果存在關(guān)于此集合的一個(gè)合一。表達(dá)式集合{P(a,y),P(x,f(b))}是可合一的，其合一為

={a/x,f(b)/y}2.3一階謂詞歸結(jié)推理(1)假設(shè)有以下前提知識(shí)：

（1）自然數(shù)是大于零的整數(shù)；（2）所有整數(shù)不是偶數(shù)就是奇數(shù)；（3）偶數(shù)除以2是整數(shù)。求證：所有自然數(shù)不是奇數(shù)就是一半為整數(shù)的數(shù)。（1）定義謂詞N(x)表示x是自然數(shù)；I(x)表示x是整數(shù)；E(x)表示x是偶數(shù)；O(x)表示x是奇數(shù)；GZ(x)表示x大于零；S(x)表示x除以2；（2）將前提條件及要求證的問(wèn)題分別以謂詞公式表示出來(lái)。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)利用歸結(jié)原理對(duì)上述子句進(jìn)行歸結(jié)推理⑧

I(t)∨E(t)③⑥歸結(jié)，

={t/y}⑨

E(t)④⑦歸結(jié)，

={t/z}⑩

I(t)⑧⑨歸結(jié)⑾

N(t)②⑩歸結(jié)⑿NIL⑤⑾歸結(jié)2.3一階謂詞歸結(jié)推理(2)用歸結(jié)的方法回答問(wèn)題：“有沒(méi)有ALPINE俱樂(lè)部的一個(gè)成員，他是一個(gè)登山運(yùn)動(dòng)員但不是一個(gè)滑雪運(yùn)動(dòng)員？”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)④⑥歸結(jié)，

={Mike/x}⑧ANSWER(Mike)

⑤⑦歸結(jié)2.3一階謂詞歸結(jié)推理(3)下列刑偵知識(shí)①John是賊;②Paul喜歡酒(wine);③Paul也喜歡奶酪(cheese);④如果Paul喜歡某物則John也喜歡某物;⑤如果某人是賊,而且他喜歡某物,則他就可能會(huì)偷竊該物。求證：John可能會(huì)偷盜什么？(1)定義謂詞①theif(x):表示x是賊；②likes(x,y):表示某人x喜歡某物y;③may_steal(x,y):表示某人x可能會(huì)偷某物y。(2)將已知事實(shí)表示成謂詞公式,并化成子句集①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)歸結(jié)⑦theif(John)∨likes(John,y)∨ANSWER(y)⑤⑥歸結(jié),={John/x,y/z}⑧l(xiāng)ikes(John,y)∨ANSWER(y)①⑦歸結(jié)⑨likes(Paul,y)∨ANSWER(y)④⑧歸結(jié)⑩ANSWER(wine)

②⑨歸結(jié),={wine/z}⑾ANSWER(cheese)

③⑨歸結(jié),={cheese/z}所以John可能會(huì)偷竊wine,也可能會(huì)偷竊cheese。2.3一階謂詞歸結(jié)推理(4)1、已知規(guī)則1：任何人的兄弟不是女性。規(guī)則2：任何人的姐妹必是女性。事實(shí)：Mary是Bill的姐妹。求證：用歸結(jié)推理方法證明Mary不是Tom的兄弟。

規(guī)則1表示為xy(brother(x,y)woman(x))事實(shí)表示為sister(Mary,Bill)作業(yè)2、用歸結(jié)法證明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一階謂詞歸結(jié)推理(5)3、證明子句集S={P∨Q,Q,P}是不可滿足的。4、用反演歸結(jié)證明定理，證明過(guò)程是這樣結(jié)束的。若（），則定理得證.5、在命題邏輯下，可以歸結(jié)的子句C1和C2，在某解釋下C1和C2為真，則其歸結(jié)式C在該解釋下（）

A.必真B.必假C.不一定作業(yè)6、設(shè)兩個(gè)子句：C1=P(x)∨Q(x)，C2=

P(a)∨T(z),在替換，其歸結(jié)式為.7、設(shè)C1=P(a)∨Q(x)∨R(x),C2=P(y)∨Q(b)，求其二元?dú)w結(jié)式。設(shè)C1=P(x)∨Q(x),C2=Q(g(x))，求其二元?dú)w結(jié)式。

2.3一階謂詞歸結(jié)推理(6)8、任何通過(guò)歷史考試并中了彩票的人是快樂(lè)的。任何肯學(xué)習(xí)或幸運(yùn)的人可以通過(guò)所有的考試，John不學(xué)習(xí)但很幸運(yùn)，任何人只要是幸運(yùn)的就能中彩。求證：John是快樂(lè)的作業(yè)9、某人被盜，派出所派出5個(gè)偵察員去調(diào)查。研究案情時(shí)，偵察員A說(shuō)：“趙和錢(qián)至少有一個(gè)人作案”；偵察員B說(shuō)：“錢(qián)和孫至少有一個(gè)人作案”；偵察員C說(shuō)：“孫和李至少有一個(gè)人作案”；偵察員D說(shuō)：“趙和孫至少有一個(gè)人與此案無(wú)關(guān)”；偵察員E說(shuō)：“錢(qián)和李至少有一個(gè)人與此案無(wú)關(guān)”。如果這5個(gè)偵察員的話都可信的，試問(wèn)誰(shuí)是盜竊犯呢？2.4一階謂詞tableau推理(1)全稱(chēng)量詞存在量詞

(t)

(t)(x)Ф

(x)ФФ{x/t}

Ф{x/t}(x)Ф

(x)ФФ{x/t}

Ф{x/t}

(t)

(p)公式中的任意項(xiàng)t一個(gè)新的參數(shù)p一階tableau擴(kuò)展規(guī)則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)對(duì)于一個(gè)自由變量xf為一個(gè)Skolem化的函數(shù),x1,…,xn是所有的tableau中的自由變量一階tableau擴(kuò)展規(guī)則﹁[(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自反規(guī)則:句子t≈t加到子句集S的tableau的任何一個(gè)分枝末尾產(chǎn)生另一個(gè)tableau．這里t是Lpar的任何項(xiàng)直觀表示為：

t≈t替換規(guī)則

如果t≈u和Φ(t)產(chǎn)生在S的tableau分枝上，Φ(u)被加到tableau后，產(chǎn)生另一個(gè)tableau．這里t和u是Lpar的任何封閉項(xiàng)．t≈uΦ(t)Φ(u)2.5

tableau推理應(yīng)用(1)數(shù)據(jù)庫(kù)修正給定一個(gè)數(shù)據(jù)庫(kù)實(shí)例r和一個(gè)完整性約束集合IC．對(duì)于IC和r的tableau，TP(IC∪r)是一個(gè)以公式集IC∪r為根節(jié)點(diǎn)的推理樹(shù)，每個(gè)tableau分枝B為I∪r形式，I∈TP(IC)，I稱(chēng)為分枝的IC部分，如果r是不相容的，tableau是封閉的，即tableau存在封閉分枝．由于IC是相容的，因此一個(gè)tableau的IC部分永遠(yuǎn)是不封閉的，只有r和IC相結(jié)合才能產(chǎn)生一個(gè)封閉的tableau?？紤]完整性約束:

x(P(x)→

yQ(x,y))和一個(gè)數(shù)據(jù)庫(kù)實(shí)例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推理應(yīng)用(2)自然語(yǔ)言理解

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推理應(yīng)用(3)電路仿真

+123輸入12g1g2g3g4g5輸出全加器電路圖門(mén)電路及其類(lèi)事實(shí)：xor_gate(g1).xor_gate(g2).and_gate(g3).and_gate(g4).or_gate(g5).所有連接類(lèi)事實(shí)：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的自動(dòng)定理證明

（4）重要的自動(dòng)推理方法：從二十世紀(jì)六十年代開(kāi)始，特別是近十年，引起了計(jì)算機(jī)科學(xué)家的廣泛興趣。（3）通用性和直觀性：對(duì)于不同的邏輯系統(tǒng)，使用相同的tableau規(guī)則，只是對(duì)公式構(gòu)造集進(jìn)行擴(kuò)展，使之更接近相應(yīng)的邏輯系統(tǒng)。（2）引入相應(yīng)的謂詞，將二元關(guān)系的性質(zhì)用邏輯公式來(lái)表示。

（1）將語(yǔ)義結(jié)構(gòu)中的二元關(guān)系顯式地表現(xiàn)出來(lái)。

1.引言1.1tableau實(shí)質(zhì)1.2Tableau方法回顧序號(hào)時(shí)間提出者內(nèi)容11955Beth提出tableau術(shù)語(yǔ)，目的是尋找一個(gè)反例21959Beth給出Gentzen的消除理論基于tableau的證明。31968Smullyan利用模型存在定理證明了tableau方法。41969Miglioli首次將tableau方法應(yīng)用于直覺(jué)邏輯。51972Fitting首次將tableau方法應(yīng)用于模態(tài)邏輯S4系統(tǒng)中。61974Surma首次將tableau方法應(yīng)用于多值?ukasiewicz邏輯中。71986Bryant提出決策圖tableau方法，能表達(dá)一個(gè)很大的可滿足的公式模型。81991Fitting出版了《FirstorderlogicsandAutomatedTheoryProving》一書(shū)，將tableau方法帶如空前繁榮階段。91994Hahnle提出子句tableau方法，采用結(jié)構(gòu)保留子句轉(zhuǎn)換方法進(jìn)行證明。102001Bertossi將tableau方法應(yīng)用于數(shù)據(jù)庫(kù)、自然語(yǔ)言理解、診斷、專(zhuān)家系統(tǒng)中。1.3研究的意義

人工智能研究的基礎(chǔ)工作，許多重要的人工智能系統(tǒng)，都以推理系統(tǒng)為其核心部分。

對(duì)人工智能的其它分枝產(chǎn)生深遠(yuǎn)的影響，提出的推理方法已被應(yīng)用于人工智能的各個(gè)領(lǐng)域。

專(zhuān)家系統(tǒng)問(wèn)題解答系統(tǒng)學(xué)習(xí)系統(tǒng)程序的自動(dòng)綜合與合成醫(yī)療系統(tǒng)信息檢索1.4研究現(xiàn)狀含量詞tableau改造技術(shù)

Fitting提出了循環(huán)控制

-規(guī)則應(yīng)用次數(shù)h的技術(shù)。increate_prove(Fml，H):－prove（Fml，[]，[]，[]，H）

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

increate_prove（Fml，NewH）。(1)相關(guān)技術(shù)和策略的研究非相關(guān)部分剪枝技術(shù)由Oppacher提出的tableau壓縮技術(shù)。

j

１

N……::封閉沒(méi)用封閉BBtableau非相關(guān)部分剪枝技術(shù)

因子分解技術(shù)因子分解技術(shù)作為模型刪除而引入。﹁p﹁qN3N2p﹁qq﹁pN1N4因子分解技術(shù)實(shí)現(xiàn)公式集{p∨q,p∨﹁q,﹁p∨q,﹁p∨﹁q}的證明過(guò)程1.4研究現(xiàn)狀子句tableau方法超tableau方法決策圖tableau方法翻譯成整數(shù)規(guī)劃的tableau方法(2)理論和方法的研究1.4研究現(xiàn)狀直覺(jué)邏輯模態(tài)邏輯多值邏輯非單調(diào)邏輯

(3)非經(jīng)典邏輯擴(kuò)展的研究數(shù)據(jù)庫(kù)修正完整性檢查查詢和變更數(shù)據(jù)庫(kù)記錄(1)數(shù)據(jù)庫(kù)方面的應(yīng)用1.5tableau應(yīng)用1.5tableau應(yīng)用

使用超tableau推理的觀點(diǎn)來(lái)解決診斷問(wèn)題。實(shí)現(xiàn)了基于tableau的診斷系統(tǒng)NIHIL(2)診斷方面的應(yīng)用

利用tableau模型生成的算子RM有效地處理了自然語(yǔ)言知識(shí)積累的問(wèn)題提出了PUHRtableau方法，有效地解決了含等詞子句的自反和替換帶來(lái)的不封閉問(wèn)題實(shí)現(xiàn)了基于tableau的RM算子及擴(kuò)展問(wèn)題的系統(tǒng)——HOU(3)自然語(yǔ)言理解方面的應(yīng)用1.5tableau應(yīng)用1.6

主要工作⑴在

-規(guī)則基礎(chǔ)上，提出對(duì)

＋-規(guī)則改進(jìn)的

＋＋-規(guī)則，結(jié)果表明，改進(jìn)后的系統(tǒng)對(duì)

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

-規(guī)則基礎(chǔ)上給出識(shí)別

-公式方法，提出了含

-公式的tableau推理的改進(jìn)策略，

-公式不再需要實(shí)例化，縮短了tableau的證明過(guò)程。

主要工作⑵在多值邏輯tableau方法研究方面，提出布爾剪枝方法，將帶符號(hào)的公式與集合的上集／下集聯(lián)系起來(lái)，使含量詞的一階多值邏輯公式的擴(kuò)展規(guī)則大大簡(jiǎn)化。并將經(jīng)典邏輯中的結(jié)構(gòu)保留子句轉(zhuǎn)換方法應(yīng)用到帶符號(hào)的多值邏輯公式中，產(chǎn)生輸入規(guī)模是線性的范式。引入極性的概念，減少冗余子句的產(chǎn)生。

⑶在增添擴(kuò)展規(guī)則的tableau方法的基礎(chǔ)上提出了一種新的含等詞tableau方法——等式合一方法。將tableau分成兩個(gè)階段，等詞單獨(dú)處理，通過(guò)提取等式合一問(wèn)題并求解解替換封閉tableau，進(jìn)一步限制了tableau的搜索空間，提高了tableau的推理效率。

主要工作主要工作⑷使用SWI-PROLOG語(yǔ)言在微機(jī)上設(shè)計(jì)實(shí)現(xiàn)了基于tableau的定理證明系統(tǒng)TableauTAP，并證明了其正確性。該系統(tǒng)可以證明不含等詞的經(jīng)典邏輯公式和多值邏輯公式，通過(guò)預(yù)處理自動(dòng)生成tableau規(guī)則，因此容易對(duì)其功能進(jìn)行擴(kuò)展。令{A1,A2,…,An}為公式的有限集合。⑴

下列分枝樹(shù)為公式{A1,A2,…,An}的一個(gè)tableau:A1A2

An⑵如果T為{A1,A2,…,An}的一個(gè)tableau，且T′為T(mén)應(yīng)用tableau推理規(guī)則后的結(jié)果，那么T′也是{A1,A2,…,An}的一個(gè)tableau。1.7tableau定義：

1

1…

n

:

n

1(y)

1(f(x1,…,xn))

y是一個(gè)自由變量

f是一個(gè)新的Skolem函數(shù)符號(hào)，

x1,…,xn是分枝中出現(xiàn)的自由變量-規(guī)則-規(guī)則-規(guī)則-規(guī)則推理規(guī)則：（1）研究現(xiàn)狀（2）問(wèn)題提出（3）本文工作（4）實(shí)驗(yàn)對(duì)比2、邏輯基礎(chǔ)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是一個(gè)新的Skolem函數(shù)符號(hào)，

x1,…,xn是分枝中出現(xiàn)的自由變量

(f(x1,…,xn)

f是一個(gè)新的Skolem函數(shù)符號(hào)，

x1,…,xn是出現(xiàn)在

中的自由變量．

1(x)

-規(guī)則

+-規(guī)則

+-規(guī)則與

-規(guī)則的區(qū)別是：在

-規(guī)則x1,…,xn是指出現(xiàn)在分枝中的自由變量，在

+-規(guī)則x1,…,xn指是出現(xiàn)在

中的自由變量．用

+-規(guī)則代替

-規(guī)則產(chǎn)生的tableau證明的長(zhǎng)度呈冪指數(shù)的減少。（1）研究現(xiàn)狀

-規(guī)則要求被Skolem化的函數(shù)符號(hào)是新的，且函數(shù)中包含分枝中出現(xiàn)的所有自由變量．顯然，由于

-規(guī)則的不確定性以及

-規(guī)則的限制，可使一個(gè)簡(jiǎn)單的證明變得很復(fù)雜，延遲了tableau的封閉時(shí)間。由于

-規(guī)則替換的任意性，可導(dǎo)致在同一tableau證明中，

-規(guī)則被多次使用，使得tableau結(jié)構(gòu)中出現(xiàn)多個(gè)自由變量。(2)問(wèn)題提出例：應(yīng)用

-、

+-、

+＋-規(guī)則證明公式集{(

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īng)用

－規(guī)則⑸(

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**應(yīng)用

+－規(guī)則⑺

P(c2)⑴

(

x)

P(x)⑶

P(x1)⑷

(

x)P(x)⑸(

y)P(y)⑹

P(c)c/x1**⑵

(

x)P(x)∨(

y)P(y)應(yīng)用

++－規(guī)則

+＋－規(guī)則為：

(f[

](x1,…,xn)f[

]是賦予的函數(shù)符號(hào)，在等價(jià)類(lèi)[

]中所有公式賦予唯一的函數(shù)符號(hào)f[

]

Σ。(3)本文工作

對(duì)于

-公式，通過(guò)skolem否定范式轉(zhuǎn)換后的公式中不再存在。因此對(duì)于

-公式的改進(jìn)，需要在否定范式的轉(zhuǎn)換謂詞change_nnf中考慮。LeanTAP系統(tǒng)TableauTAP系統(tǒng)

SWI-Prolog語(yǔ)言change_nnf(ex(X,Fml)，F(xiàn)reeV,NNF,Paths):-!，copy_term((X,Fml,FreeV)，(Fml,Fml1,FreeV))，copy_term((X,Fml,FreeV)，(a,Fml2,FreeV))，nnf(Fml1，F(xiàn)reeV，NNF，Paths)。（4）系統(tǒng)的實(shí)現(xiàn)及實(shí)驗(yàn)對(duì)比問(wèn)題序號(hào)

-規(guī)則

+-規(guī)則

++-規(guī)則節(jié)點(diǎn)數(shù)(個(gè))時(shí)間(毫秒)節(jié)點(diǎn)數(shù)(個(gè))時(shí)間(毫秒)節(jié)點(diǎn)數(shù)(個(gè))時(shí)間(毫秒)1301403014018852411683615036150326872687268747520175201531605180304892106015464917034130341307104280104280581708331503315020100927135271352713510872098720946140

實(shí)驗(yàn)結(jié)果

可以看出，從tableau擴(kuò)展節(jié)點(diǎn)數(shù)和封閉時(shí)間上進(jìn)行了比較，其中有2個(gè)問(wèn)題，應(yīng)用

+、

++規(guī)則沒(méi)有變化，其中有6個(gè)問(wèn)題，應(yīng)用

++規(guī)則后，節(jié)點(diǎn)數(shù)和時(shí)間上都有較大幅度的減少。3、語(yǔ)義tableau中γ-規(guī)則的改進(jìn)(1)研究現(xiàn)狀(2)問(wèn)題提出(3)本文的工作(4)實(shí)驗(yàn)對(duì)比

如果一個(gè)tableau分枝B包含一個(gè)公式P(x)，在tableau過(guò)程中，x必然出現(xiàn)在某些分枝上，為了封閉這些分枝需要多次對(duì)x進(jìn)行實(shí)例化(

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)研究現(xiàn)狀

在tableau證明中,

-公式對(duì)其中包含的自由變量需要進(jìn)行多次不同的實(shí)例化。典型的例子是群論中的結(jié)合律(

x)(

y)(

z)((x·y)·z

x·(y·z))，應(yīng)用該定律即使證明一個(gè)非常簡(jiǎn)單的定理，也要對(duì)其中的x、y、z進(jìn)行多次不同的實(shí)例化替換。

(2)問(wèn)題提出在tableau實(shí)現(xiàn)時(shí)，對(duì)

-規(guī)則應(yīng)用次數(shù)的限制致關(guān)重要:限制的次數(shù)太少，不能滿足推理需要的實(shí)例，使一個(gè)恒真的公式得不到tableau證明。限制的次數(shù)過(guò)多，由于

-規(guī)則使用次數(shù)的不確定性，必然會(huì)導(dǎo)致大量的冗余推理產(chǎn)生，使證明過(guò)程的搜索空間膨脹。

令Γ為理論，φ為tableauT的一個(gè)分枝B上的公式，對(duì)于變量x,通過(guò)向T的分枝B中增加(

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

用

-規(guī)則，x是引入的自由變量；或⑵

關(guān)于x的全稱(chēng)公式ψ應(yīng)用

-，

-，

-規(guī)則。R是識(shí)別

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

一個(gè)公式G(x)被識(shí)別為關(guān)于x的

-公式，那么G(x′)、G(x″)、…能被加入到分枝中，而不影響其它分枝或產(chǎn)生新分枝。一旦一個(gè)公式被識(shí)為

-公式，那么尋找一個(gè)封閉tableau的替換

就變得比較容易：對(duì)于

-公式中的變量不需要實(shí)例化。

令R為識(shí)別

-公式的方法，帶分枝B1,…,Bk的自由變量tableauT是封閉的，當(dāng)且僅當(dāng)存在替換σ1,…,σk使得：⑴對(duì)于1≤i≤k，公式Fi,?Gi∈Bi,并且Fiσi＝Giσi。⑵只有變量x對(duì)于公式Fi,Gi∈BiFj,Gj∈Bj是

-公式時(shí)，存在替換σ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)被識(shí)別為

-公式，因此P(y)不再需要實(shí)例化，可立即封閉。這樣會(huì)使tableau過(guò)程縮短，搜索空間減小。例：{(

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)＊如果等式⑻應(yīng)用到⑷的過(guò)程中，

{g(a)/x2}代替

{a/x2}將產(chǎn)生錯(cuò)誤的方法，即

⑽*

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

⑽P(g(f(a)),b)那么tableau不能封閉。tableau在替換{a/x1，a/x2}下是封閉的．因此Fitting方法也存在著不確定性問(wèn)題，隨著tableau推進(jìn)順序的不同，可導(dǎo)致不同的結(jié)果。該方法很難用于機(jī)器實(shí)現(xiàn)，并且不可避免地產(chǎn)生回溯。利用的識(shí)別

-公式的方法，等式⑹被識(shí)別為關(guān)于x1的

-公式，因此x1不再需要實(shí)例化，例子的tableau過(guò)程中的⑽⑾⑿可以刪除，通過(guò)替換{a/x2}即可封閉。

用VisualProlog語(yǔ)言在Windows環(huán)境下進(jìn)行了系統(tǒng)UniTAP的實(shí)現(xiàn)，程序中將識(shí)別出的

-變量保存在一個(gè)表中，可以對(duì)表中的變量進(jìn)行實(shí)例化，使分枝中的實(shí)例互不影響。使用的謂詞如下：

(4)實(shí)驗(yàn)對(duì)比Prove（

Fml，UnExp，Lits，DisV，F(xiàn)reeV，UnivV，VarLim）自由變量被實(shí)例化的最大次數(shù)

出在Fml中的全稱(chēng)變量表出現(xiàn)在目前分枝中的自由變量表

除

變量以外的所有Prolog項(xiàng)出現(xiàn)在目前分枝中的文字表

擴(kuò)展過(guò)程中的公式待擴(kuò)展的源公式

利用LeanTAP系統(tǒng)和UniTAP系統(tǒng)處理Pelletier問(wèn)題的實(shí)驗(yàn)結(jié)果Pelletier問(wèn)題序號(hào)VarLim限定次數(shù)LeanTAP系統(tǒng)UniTAP系統(tǒng)封閉分枝數(shù)運(yùn)行時(shí)間(msec)封閉分枝數(shù)運(yùn)行時(shí)間(msec)171142201013218219018519243302202206318017621284626304222730742902314243421024633608202092535409333226316563122382748686843328354012374292116096501302427622333135834346532310487637733111218511034526710981124303541149112036633513302

-公式不再需要實(shí)例化，大大縮短了tableau的證明過(guò)程，減少封閉分枝，提高了推理效率。另外在非經(jīng)典邏輯中的識(shí)別

-公式的方法與經(jīng)典邏輯類(lèi)似，因此只要稍加修改就可將該方法擴(kuò)展到非經(jīng)典邏輯中。

含等詞的tableau方法研究現(xiàn)狀問(wèn)題提出本文工作實(shí)例對(duì)比分析小結(jié)4、利用等式合一處理含等詞tableauJeffrey方法（1）含等詞的tableau方法分析t≈s

s≈t

[t]

[t]

[s]

[s]

Jeffrey含等詞擴(kuò)展規(guī)則

存在問(wèn)題無(wú)關(guān)公式的數(shù)目隨著謂詞元數(shù)的增加呈冪指數(shù)增長(zhǎng)擴(kuò)展規(guī)則是對(duì)稱(chēng)的，它的應(yīng)用不受限制。這就導(dǎo)致了在推理過(guò)程中，產(chǎn)生大量的無(wú)關(guān)公式Reeves方法（1）含等詞的tableau方法分析P(s1,…,sn)

P(t1,…,tn)

(s1≈t1)

…

(sn≈tn)

(s1≈t1)

…

(sn≈tn)

Reeves含等詞擴(kuò)展規(guī)則

f(s1,…,sn)≈f(t1,…,tn)優(yōu)點(diǎn)：對(duì)封閉分枝的搜索更直接存在問(wèn)題：如果一個(gè)分枝包含幾個(gè)等式和不等式，新的擴(kuò)展規(guī)則也可能被看成同樣的等式和不等式來(lái)擴(kuò)展，這樣連續(xù)不斷的新的擴(kuò)展分枝被加入到tableau中。分枝的增長(zhǎng)隨著在分枝中等式的數(shù)目的增加，呈冪指數(shù)的增長(zhǎng)，因此Reeves方法不利于機(jī)器實(shí)現(xiàn)。Fitting方法（1）含等詞的tableau方法分析t≈s

s≈t

[t′]

[t′]

(

[s])μ(

[s])μ

含等詞自由變量tableau擴(kuò)展規(guī)則μ是t和t′的MGU，μ應(yīng)用到整個(gè)tableau

存在問(wèn)題：存在著不確定性問(wèn)題,隨著tableau推進(jìn)順序的不同，可導(dǎo)致不同的結(jié)果很難用于機(jī)器實(shí)現(xiàn)，并且不可避免地進(jìn)行回溯

在增添擴(kuò)展規(guī)則的tableau方法的基礎(chǔ)上提出一種新的含等詞tableau算法——等式合一方法。在該方法中，將tableau分成兩個(gè)階段，等詞單獨(dú)處理，通過(guò)提取等式合一問(wèn)題并求解解替換封閉tableau，該方法進(jìn)一步限制了tableau的搜索空間，提高了tableau的推理效率。（2）問(wèn)題提出

等式合一問(wèn)題<E，s，t>包含形如(

x1)…(

xn)(l≈r)的等式的有窮集合E、項(xiàng)s和t。一個(gè)替換

為等式合一問(wèn)題的解當(dāng)且僅當(dāng)E

╞(s

≈t

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

令B為一個(gè)tableau分枝，等式合一問(wèn)題集合包含集合序?qū)?lt;E(B)，P(B)>，其中:⑴集合E(B)定義為：{s≈t：s≈t∈B}

E(B)；⑶對(duì)于B上的每個(gè)不等式

(s≈t),{s

,t

)}

P(B)。⑵對(duì)于B上的潛在封閉原子對(duì)p(s1,…,sn)和

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

使得{s1

≠t1

∨…∨sn

≠tn

}

P(B)；等式合一問(wèn)題集合分階段tableau

將tableau擴(kuò)展分成兩個(gè)階段。第一階段是在處理等詞之前，應(yīng)用tableau擴(kuò)展規(guī)則，將所有的tableau擴(kuò)展完成，在這個(gè)過(guò)程中要求對(duì)

-規(guī)則應(yīng)用次數(shù)進(jìn)行限制。第二階段是處理等詞，通過(guò)適當(dāng)?shù)氖侄危拗频仍~的使用，以避免無(wú)關(guān)公式的產(chǎn)生。

分階段tableau方法不需要在等詞應(yīng)用規(guī)則和其它擴(kuò)展規(guī)則之間轉(zhuǎn)換，因此在第一階段完成以后，許多公式不再需要。從第二階段開(kāi)始只需要考慮等式、不等式以及潛在的封閉原子對(duì)，這樣使含等詞的tableau在一個(gè)更適合的數(shù)據(jù)結(jié)構(gòu)P(B)和E(B)下進(jìn)行?；舅枷耄和陚湫裕喝绻?/p>

是不可滿足的，q足夠大，那么T是T2封閉的。可靠性：如果T是T2封閉的，那么公式

是不可滿足的。T是關(guān)于公式

的tableau，q是

-規(guī)則應(yīng)用的限定次數(shù)，利用等式合一解替換封閉tableauTableauT是T2封閉的，當(dāng)存在一個(gè)基替換

，對(duì)于T上的每一個(gè)分枝B，存在一個(gè)析取（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算法(計(jì)算集合<t>的等價(jià)序列的近似算法)輸入：項(xiàng)t、等式集合E(B)、n的最高次數(shù)輸出：項(xiàng)t的等價(jià)序列集合<t>等式合一問(wèn)題的實(shí)現(xiàn)算法（4）實(shí)例對(duì)比分析(

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

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

為不可滿足的任意公式．tableau第一階段的擴(kuò)展如下：

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

*

后面標(biāo)注“√”的為不再使用的公式，第一階段完成后，tableau擴(kuò)展已經(jīng)完成，但tableau沒(méi)有封閉。

例：證明公式設(shè)未封閉分枝為B，B轉(zhuǎn)換成集合E(B)和P(B)。

E(B)={g(f(x))≈c,f(x)≈g(x)}P(B)={g(g(a))≠g(f(b))}Tableau的第二階段轉(zhuǎn)換成計(jì)算<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方法證明同一公式為重言式，

-公式的使用次數(shù)必須提高。（2）在同一啟發(fā)搜索算法下，證明不等式g(g(a))≠g(f(b))的不可滿足性，將產(chǎn)生15個(gè)中間等式，并需要幾次的自由變量替換。（3）如果使用Jeffrey方法證明同一公式為重言式，等式規(guī)則的應(yīng)用次數(shù)依賴(lài)于使用等式的次序，最好的情況下只需要2個(gè)分枝即封閉，然而在較差的情況下可以產(chǎn)生幾百個(gè)分枝。

提出利用等式合一處理含等詞tableau方法，將tableau擴(kuò)展分成兩個(gè)階段。第一階段是在處理等詞之前，應(yīng)用tableau擴(kuò)展規(guī)則，將所有的tableau擴(kuò)展完成，在這個(gè)過(guò)程中要求對(duì)

規(guī)則應(yīng)用次數(shù)進(jìn)行限制。第二階段是處理等詞，通過(guò)提取等式合一問(wèn)題并求解解替換封閉tableau，在啟發(fā)式的幫助下計(jì)算等價(jià)類(lèi)的方法，限制等詞的使用，以避免無(wú)關(guān)公式的產(chǎn)生，在效率和實(shí)現(xiàn)上都有較大的提高。

（5）小結(jié)

一是二是將計(jì)算等價(jià)類(lèi)的結(jié)果以樹(shù)的結(jié)構(gòu)進(jìn)行存儲(chǔ)，利用樹(shù)的特點(diǎn)，進(jìn)行搜索的優(yōu)化，提高推理效率。改進(jìn)啟發(fā)式算法，提高計(jì)算等價(jià)類(lèi)的速度。5、多值邏輯語(yǔ)義tableau方法(1)含量詞的一階多值邏輯Tableau(2)問(wèn)題提出(3)利用布爾集格對(duì)tableau方法的改進(jìn)(4)含廣義量詞的四值邏輯tableau實(shí)例(5)實(shí)例分析(6)多值邏輯正則公式的tableau方法(7)小結(jié)

(Q(

))-1(S)={I

I

N，Q(

)(I)

S}(Q(

))-1({0})={{0},{0,},{0,1},{0,,1}}(1)含量詞的一階多值邏輯Tableau2121擴(kuò)展規(guī)則：符號(hào)引入：

含量詞的tableau方法是由Carnielli（1987）引入，后來(lái)由Zabel(1993)在理論上找到了可滿足的擴(kuò)展規(guī)則，并給出了可靠性和完備性的證明。然而對(duì)于自動(dòng)定理證明來(lái)說(shuō)，其實(shí)現(xiàn)難度非常大，為此找出一種擴(kuò)展分枝更少的有效推理方法。提出了布爾剪枝方法，將帶符號(hào)的公式與集合的上集／下集聯(lián)系起來(lái)，使含量詞的一階公式的擴(kuò)展規(guī)則大大簡(jiǎn)化。通過(guò)對(duì)布爾剪枝方法的進(jìn)一步探討，建立了一類(lèi)特殊一階多值邏輯正則公式的更為簡(jiǎn)捷的tableau推理方法，該方法使得含量詞的一階多值邏輯tableau推理類(lèi)同于經(jīng)典邏輯tableau方法。(2)問(wèn)題提出在多值邏輯中例：在一階三值Kleene邏輯中，可以對(duì){0}(

x)

(x)進(jìn)行擴(kuò)展，其中(Q(

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

},{0,1},{0,,1}}。擴(kuò)展結(jié)果如下：{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，產(chǎn)生的關(guān)于布爾集格2N的集合的上集為U(F)={X

X

N,X∩F

}。定義I，

I

N，產(chǎn)生的關(guān)于布爾集格2N的集合的下集為D(I)={X

X

N,

X

I}。（3）利用布爾集格對(duì)tableau方法的改進(jìn)⑴如果(Q(

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

x)

(x)是可滿足的當(dāng)且僅當(dāng)對(duì)于新的Skolem常數(shù)c，F(xiàn)

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

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

x)

(x)是可滿足的當(dāng)且僅當(dāng)對(duì)于所有的基項(xiàng)t，I

(t)是可滿足的。

設(shè)N為有窮真值集，S

N，定理定義例子中，一階三值Kleene邏輯中，

因?yàn)?Q(

))-1({0})=U({0})={{0},{0,},{0,1},{0,,1}}，因此規(guī)則可簡(jiǎn)化為：

{0}(

x)

(x){0}

(c)

另外，因?yàn)?Q(

))-1({0})=D({0})={{0}}，因此規(guī)則

{0}(

x)

(x){0}

(t)是成立的。這一結(jié)論也是與經(jīng)典情況一致的。2121

將含量詞的tableau方法與布爾集格相結(jié)合，簡(jiǎn)化了tableau的擴(kuò)展分枝，在本章中我們稱(chēng)之為布爾剪枝。在效率和實(shí)現(xiàn)上都有較大的提高時(shí)間效率空間效率Zabel方法O(nk)O(n*k)布爾剪枝方法O(n*k)O(n)例：考慮真值集合FOUR={⊥,f,t,?}，定義量詞Π，Q(Π)=，這里

為格中的交操作?！蚮t{⊥,f}{}{⊥}{f}{t}{?}{⊥,t}{f,t}{⊥,?}{f,?}{t,?}{⊥,f,t}{⊥,f,?}{⊥,t,?}{f,t,?}FOUR四值布爾集格四值邏輯格結(jié)構(gòu)（4）含廣義量詞的四值邏輯tableau實(shí)例?

以{⊥}為例，tableau擴(kuò)展結(jié)果如下：{⊥}

(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(Σ)=?

設(shè)L=<N,?,?>為真值有窮集合N上的格，定義分布量詞Π和Σ如下：則有下列式子成立：定理⑴如果i∈MI(L)，那么(Q－１(Π))({i})=U({i})∩(D(

i)∪{

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

i)=U(

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

m))∩(D(

i)∪{

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

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

i)=U(

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

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

i)=D(

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

i)∪{

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

i)=U(

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