第5章-基于謂詞邏輯的機(jī)器推理課件

第5章基于謂詞邏輯的機(jī)器推理12/30/20221第5章基于謂詞邏輯的機(jī)器推理12/29/20221目錄5.0機(jī)器推理概述5.1一階謂詞邏輯5.2歸結(jié)演繹推理5.3應(yīng)用歸結(jié)原理求取問(wèn)題答案5.4歸結(jié)策略5.5歸結(jié)反演程序舉例*5.6Horn子句歸結(jié)與邏輯程序5.7非歸結(jié)演繹推理12/30/20222目錄5.0機(jī)器推理概述12/29/202225.0機(jī)器推理概述（1）機(jī)器推理：就是計(jì)算機(jī)推理，也稱(chēng)自動(dòng)推理。它是人工智能的核心課題之一。推理是人腦的一個(gè)基本功能和重要功能。幾乎所有的人工智能領(lǐng)域都與推理有關(guān)。因此，要實(shí)現(xiàn)人工智能，就必須將推理的功能賦予機(jī)器，實(shí)現(xiàn)機(jī)器推理。自動(dòng)定理證明：是機(jī)器推理的一種重要應(yīng)用，它是利用計(jì)算機(jī)證明非數(shù)值性的結(jié)果，很多非數(shù)值領(lǐng)域的任務(wù)如醫(yī)療診斷、信息檢索、規(guī)劃制定和難題求解等方法都可以轉(zhuǎn)化一個(gè)定理證明問(wèn)題。12/30/202235.0機(jī)器推理概述（1）機(jī)器推理：自動(dòng)定理證明：12/29自動(dòng)定理證明的基本方法：5.0機(jī)器推理概述（2）定理證明器：它是研究一切可判定問(wèn)題的證明方法。魯濱遜的歸結(jié)原理。人機(jī)交互進(jìn)行定理證明：計(jì)算機(jī)作為數(shù)學(xué)家的輔助工具，用計(jì)算機(jī)幫助人完成手工證明中的難以完成的煩雜的大量計(jì)算推理和窮舉。典型代表：四色定理的證明。判定法：該方法是對(duì)一類(lèi)問(wèn)題找出統(tǒng)一的計(jì)算機(jī)上可實(shí)現(xiàn)的算法。典型代表：數(shù)學(xué)家吳文俊教授——吳氏方法。自然演繹法：該方法依據(jù)推理規(guī)則從前提和公理中可以推出許多定理，如果待證明的定理在其中則定理得證。典型代表：LT程序、證明平面幾何的程序。12/30/20224自動(dòng)定理證明的基本方法：5.0機(jī)器推理概述（2）定理證明器基于歸結(jié)原理的自動(dòng)定理證明過(guò)程：5.0機(jī)器推理概述（3）定理的自然語(yǔ)言描述定理的謂詞公式描述子句集生成子句集定理得證應(yīng)用歸結(jié)規(guī)則＋歸結(jié)策略自然語(yǔ)言處理生成謂詞公式已知前提：F1：自然數(shù)都是大于零的整數(shù)。F2：所有整數(shù)不是偶數(shù)就是奇數(shù)。F3：偶數(shù)除以2是整數(shù)。結(jié)論G：所有自然數(shù)不是奇數(shù)就是除以2為整數(shù)的數(shù)。定理的謂詞公式描述：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)(I(s(x))O(x)))12/30/20225基于歸結(jié)原理的自動(dòng)定理證明過(guò)程：5.0機(jī)器推理概述（3）定5.1一階謂詞邏輯5.1.1謂詞、函數(shù)、量詞5.1.2謂詞公式5.1.3謂詞邏輯中的形式演繹推理12/30/202265.1一階謂詞邏輯5.1.1謂詞、函數(shù)、量詞12/29/5.1.1謂詞、函數(shù)、量詞（1）命題（proposition）：是具有真假意義的語(yǔ)句。命題代表人們進(jìn)行思維時(shí)的一種判斷，或者是否定，或者是肯定。命題可以用命題符號(hào)表示，如：用命題符號(hào)可以表示簡(jiǎn)單的邏輯關(guān)系和推理。P:今天天氣好Q:去旅游S1：我有名字S2：你有名字PQ：表示如果今天天氣好，就去旅游。此時(shí)，如果P（今天天氣好）成立，則可以得到結(jié)論Q（去旅游）12/30/202275.1.1謂詞、函數(shù)、量詞（1）命題（propositio5.1.1謂詞、函數(shù)、量詞（2）對(duì)于復(fù)雜的知識(shí)，命題符號(hào)能力不夠。無(wú)法把所描述的客觀事物的結(jié)構(gòu)及邏輯特征反映出來(lái)。無(wú)法把不同事物間的共同特征表達(dá)出來(lái)。F：老李是小李的父親。S1：我有名字S2：你有名字所有的人都有名字：S1S2S3…

12/30/202285.1.1謂詞、函數(shù)、量詞（2）對(duì)于復(fù)雜的知識(shí)，命題符號(hào)能5.1.1謂詞、函數(shù)、量詞（3）謂詞(predicate)：一般形式為P(x1,x2,…,

xn)其中，P為謂詞名，用于刻畫(huà)個(gè)體的性質(zhì)、狀態(tài)或個(gè)體間的關(guān)系。

x1,x2,…,xn是個(gè)體，表示某個(gè)獨(dú)立存在的事物或者某個(gè)抽象的概念。例如：S(x):x是學(xué)生；P(x,y):x是y的雙親。個(gè)體變?cè)淖兓秶Q(chēng)為個(gè)體域。包攬一切事物的集合稱(chēng)為全總個(gè)體域。12/30/202295.1.1謂詞、函數(shù)、量詞（3）謂詞(predicate)：5.1.1謂詞、函數(shù)、量詞（4）函數(shù)：為了表達(dá)個(gè)體之間的對(duì)應(yīng)關(guān)系，引入數(shù)學(xué)中函數(shù)概念和記法。用形如f(x1,x2,…,xn)來(lái)表示個(gè)體變?cè)獙?duì)應(yīng)的個(gè)體y，并稱(chēng)之為n元個(gè)體函數(shù)，簡(jiǎn)稱(chēng)函數(shù)。f是函數(shù)符號(hào)。函數(shù)增強(qiáng)了謂詞的表達(dá)能力函數(shù)father(x):值為x的父親。謂詞Doctor(father(Li)):表示Li的父親是醫(yī)生，值為真或假。符號(hào)約定：謂詞符號(hào)－大寫(xiě)字母；P(x,y)函數(shù)符號(hào)－小寫(xiě)字母；f(x)個(gè)體變?cè)?hào)－x、y、z、u、v……個(gè)體常元符號(hào)－a、b、c…….。P(a,b)12/30/2022105.1.1謂詞、函數(shù)、量詞（4）函數(shù)：為了表達(dá)個(gè)體之間的對(duì)邏輯聯(lián)結(jié)詞聯(lián)結(jié)詞優(yōu)先級(jí)應(yīng)用?否定1?p,非p^合取2p^q,不僅p,而且q、既p,又q、一邊p,一邊q、雖然p,但是q∨析取2相容的或p∨q,排斥的或p∨?q^?p∨q蘊(yùn)含3p->q，q是p的必要條件，p是q的充分條件。只要p就q、p僅當(dāng)q、只有q才p<->等價(jià)3p<->q，p和q互為充分必要條件P當(dāng)且僅當(dāng)q同級(jí)從左向右順序演算12/30/202211邏輯聯(lián)結(jié)詞聯(lián)結(jié)詞優(yōu)先級(jí)應(yīng)用?否定1?p,非p^合取2p^5.1.1謂詞、函數(shù)、量詞（5）表示“對(duì)個(gè)體域中所有的（或任一個(gè)）個(gè)體”。記為x所有、一切、全體、凡是等詞統(tǒng)稱(chēng)為全稱(chēng)量詞全稱(chēng)量詞：表示“在個(gè)體域中存在個(gè)體”。記為x存在、有些、有的、至少有一個(gè)等詞統(tǒng)稱(chēng)為存在量詞存在量詞：如：“凡是人都有名字”

用M（x）表示“x是人”，N（x）表示“x有名字”x（M（x）N（x））如：“存在不是偶數(shù)的整數(shù)”用G（x）表示“x是整數(shù)”，E（x）表示“x是偶數(shù)”x（G（x）?E（x））

12/30/2022125.1.1謂詞、函數(shù)、量詞（5）表示“對(duì)個(gè)體域中所有的（或5.1.1謂詞、函數(shù)、量詞（6）用謂詞表示命題時(shí)，一般取全總個(gè)體域，再采用使用限定謂詞的方法來(lái)指出每個(gè)個(gè)體變?cè)膫€(gè)體域。(2)對(duì)存在量詞，把限定詞作為一個(gè)合取項(xiàng)加入。即x(P(x)…)例5.2：對(duì)于所有的自然數(shù)，均有x+y>x

xy（N（x）N（y）S(x,y,x)）例5.3：某些人對(duì)某些食物過(guò)敏xy(M(x)N(y)G(x,y))(1)對(duì)全稱(chēng)量詞，把限定詞作為蘊(yùn)含式之前件加入。即x（P（x）…）例5.2：對(duì)于所有的自然數(shù)，均有x+y>x

也可以用函數(shù)h（x，y）來(lái)表示x與y的和

xy（N（x）N（y）G(h(x,y),x)）12/30/2022135.1.1謂詞、函數(shù)、量詞（6）用謂詞表示命題時(shí)，一般取全5.1.1謂詞、函數(shù)、量詞（7）例5.1：不存在最大的整數(shù)，我們可以把它表示為：

?x(G(x)y(G(y)D(x，y)))

x(G(x)y(G(y)D(y，x)))用謂詞表示命題時(shí)，形式并不是固定的。12/30/2022145.1.1謂詞、函數(shù)、量詞（7）例5.1：不存在最大的整數(shù)5.1.1謂詞、函數(shù)、量詞（8）練習(xí)：用謂詞公式表示下述命題。已知前提：（1）自然數(shù)都是大于零的整數(shù)。（2）所有整數(shù)不是偶數(shù)就是奇數(shù)。（3）偶數(shù)除以2是整數(shù)。結(jié)論：所有自然數(shù)不是奇數(shù)就是除以2為整數(shù)的數(shù)。首先定義如下謂詞：N(x):x是自然數(shù)。I(x):x是整數(shù)。E(x):x是偶數(shù)。

O(x):x是奇數(shù)。GZ(x):x大于零。s(x):x除以2。12/30/2022155.1.1謂詞、函數(shù)、量詞（8）練習(xí)：用謂詞公式表示下述命題5.1.1謂詞、函數(shù)、量詞（9）將上述各語(yǔ)句翻譯成謂詞公式：（1）自然數(shù)都是大于零的整數(shù)。F1:x(N(x)GZ(x)I(x))（2）所有整數(shù)不是偶數(shù)就是奇數(shù)。F2:x(I(x)(E(x)O(x)))（3）偶數(shù)除以2是整數(shù)。F3:x(E(x)I(s(x)))所有自然數(shù)不是奇數(shù)就是除以2為整數(shù)的數(shù)。G:x(N(x)(I(s(x))O(x)))

12/30/2022165.1.1謂詞、函數(shù)、量詞（9）將上述各語(yǔ)句翻譯成謂詞公式5.1.2謂詞公式（1）定義1：項(xiàng)（1）個(gè)體常元和變?cè)际琼?xiàng)。（2）f是n元函數(shù)符號(hào)，若t1，t2，…，tn是項(xiàng)，則f(t1，t2，…，tn)是項(xiàng)。（3）只有有限次使用（1），（2）得到的符號(hào)串才是項(xiàng)。用謂詞、量詞及真值連結(jié)詞可以表達(dá)相當(dāng)復(fù)雜的命題，我們把命題的這種符號(hào)表達(dá)式稱(chēng)為謂詞公式。12/30/2022175.1.2謂詞公式（1）定義1：項(xiàng)（1）個(gè)體常元和變?cè)际?.1.2謂詞公式（2）定義2：原子公式設(shè)P為n元謂詞符號(hào)，t1，t2，…，tn為項(xiàng)，P(t1，t2，…，tn)稱(chēng)為原子謂詞公式，簡(jiǎn)稱(chēng)原子或原子公式。從原子謂詞公式出發(fā)，通過(guò)命題聯(lián)結(jié)詞和量詞，可以組成復(fù)合謂詞公式。12/30/2022185.1.2謂詞公式（2）定義2：原子公式設(shè)P為n元謂詞符號(hào)5.1.2謂詞公式（3）定義3：謂詞公式（1）原子公式是謂詞公式。（2）若A、B是謂詞公式，則?A，AB，AB，AB，A←→B，xA，xA也是謂詞公式。（3）只有有限步應(yīng)用（1）（2）生成的公式才是謂詞公式。謂詞公式亦稱(chēng)為謂詞邏輯中的合適（式）公式，記為Wff。由項(xiàng)的定義，當(dāng)t1，t2，…，tn全為個(gè)體常元時(shí)，所得的原子謂詞公式就是原子命題公式（命題符號(hào)）。所以全體命題公式也是謂詞公式。

12/30/2022195.1.2謂詞公式（3）定義3：謂詞公式（1）原子公式是謂5.1.2謂詞公式（4）轄域：緊接于量詞之后被量詞作用（即說(shuō)明）的謂詞公式稱(chēng)為該量詞的轄域。指導(dǎo)變?cè)毫吭~后的變?cè)獮橹笇?dǎo)變?cè)?。約束變?cè)涸谝粋€(gè)量詞轄域中與該量詞的指導(dǎo)變?cè)嗤淖冊(cè)Q(chēng)為約束變?cè)?。自由變?cè)褐^詞公式中除了約束變?cè)獾淖冊(cè)?/p>

（1）xP(x)（2）y(G(y)D(x,y))（3）xG(x)P(x)指導(dǎo)變?cè)s束變?cè)s束變?cè)s束變?cè)杂勺冊(cè)杂勺冊(cè)?2/30/2022205.1.2謂詞公式（4）轄域：緊接于量詞之后被量詞作用（即5.1.2謂詞公式（5）一個(gè)變?cè)谝粋€(gè)公式中既可以約束出現(xiàn)，也可以自由出現(xiàn)，為了避免混淆，通過(guò)改名規(guī)則改名：對(duì)需要改名的變?cè)?，?yīng)同時(shí)更改該變?cè)诹吭~及其轄域中的所有出現(xiàn)。新變?cè)?hào)必須是量詞轄域內(nèi)原先沒(méi)有的，最好是公式中也未出現(xiàn)過(guò)的。xG(x)P(x)改為xG(x)P(y)或yG(y)P(x)12/30/2022215.1.2謂詞公式（5）一個(gè)變?cè)谝粋€(gè)公式中既可以約束出現(xiàn)5.1.2謂詞公式（6）謂詞公式與命題的區(qū)別與聯(lián)系謂詞公式是命題函數(shù)。一個(gè)謂詞公式中所有個(gè)體變?cè)涣炕ㄔ谥^詞前加上量詞），謂詞公式就變成了一個(gè)命題。從謂詞公式得到命題的兩種方法：給謂詞中的個(gè)體變?cè)雮€(gè)體常元；把謂詞中的個(gè)體變?cè)苛炕?。例：謂詞公式P（x）表示“x是素?cái)?shù)”P(pán)（a）

xP（x）,xP（x）都是命題12/30/2022225.1.2謂詞公式（6）謂詞公式與命題的區(qū)別與聯(lián)系例：謂詞5.1.2謂詞公式（7）一階謂詞：僅個(gè)體變?cè)涣炕闹^詞。二階謂詞：不僅個(gè)體變?cè)涣炕?，函?shù)符號(hào)和謂詞符號(hào)也被量化。如：

P

xP（x）以下兩種命題在個(gè)體域?yàn)橛邢藜瘯r(shí)（n個(gè)元素），有下面的等價(jià)式全稱(chēng)命題：

xP(x)等價(jià)于P(a1)P(a2)…P(an)

特稱(chēng)命題

xG(x)等價(jià)于P(a1)P(a2)…P(an)12/30/2022235.1.2謂詞公式（7）一階謂詞：僅個(gè)體變?cè)涣炕闹^詞。5.1.2謂詞公式（8）定義4：合取范式（ConjunctiveNormalForm）

設(shè)A為如下形式的謂詞公式：B1B2…

Bn其中Bi（i=1,2,…，n）形如L1

L2…

Lm，Lj（j=1，2,…，m）為原子公式或其否定，則A稱(chēng)為合取范式。例(P(x)

Q(y))

(?P(x)Q(y)R(x,y))

(?Q(x)?R(x,y))就是一個(gè)合取范式應(yīng)用邏輯等價(jià)式，任一謂詞公式可化為與之等價(jià)的合取范式，一個(gè)謂詞的合取范式不唯一12/30/2022245.1.2謂詞公式（8）定義4：合取范式（Conjunct5.1.2謂詞公式（9）定義5：析取范式（DisjunctiveNormalForm）設(shè)A為如下形式的謂詞公式：B1

B2…

Bn其中Bi（i=1,2,…，n）形如L1

L2

…

Lm，Lj（j=1，2,…，m）為原子公式或其否定，則A稱(chēng)為析取范式。例(P(x)?Q(y)R(x,y))(?P(x)Q(y))(?P(x)R(x,y))就是一個(gè)析取范式應(yīng)用邏輯等價(jià)式，任一謂詞公式可化為與之等價(jià)的析取范式，一個(gè)謂詞的析取范式不唯一12/30/2022255.1.2謂詞公式（9）定義5：析取范式（Disjunct5.1.2謂詞公式（10）*謂詞公式的解釋?zhuān)簩?duì)謂詞公式中的各種變量指定特殊的常量去替代。設(shè)D為謂詞公式P的個(gè)體域，若對(duì)P中的個(gè)體常量、函數(shù)和謂詞按如下規(guī)定賦值：（1）為每個(gè)個(gè)體常量指派D中的一個(gè)元素；（2）為每個(gè)n元函數(shù)指派一個(gè)從Dn到D的映射，其中Dn＝{(x1,x2,…,xn)|x1,x2,…,xn∈D}（3）為每個(gè)n元謂詞指派一個(gè)從Dn到{F,T}的映射。稱(chēng)這些指派(謂詞公式的解釋)為公式P在D上的一個(gè)解釋。當(dāng)被解釋的謂詞公式在特定解釋下真值為真，稱(chēng)這個(gè)解釋滿足這個(gè)謂詞公式。12/30/2022265.1.2謂詞公式（10）*謂詞公式的解釋?zhuān)簩?duì)謂詞公式中的謂詞公式的解釋*用某個(gè)解釋解釋一個(gè)謂詞公式，就是將解釋中的各個(gè)值帶到謂詞公式中去，要全部取到。約束出現(xiàn)的變?cè)≈店P(guān)系與量詞性質(zhì)有關(guān)，當(dāng)指導(dǎo)變?cè)南鄳?yīng)量詞為存在量詞，此時(shí)每個(gè)個(gè)體域的取值所對(duì)應(yīng)的謂詞真值的關(guān)系為或關(guān)系，也就是說(shuō)在個(gè)體域中有一個(gè)特定點(diǎn)解釋該謂詞公式即可。當(dāng)指導(dǎo)變?cè)南鄳?yīng)量詞為全稱(chēng)量詞，此時(shí)每個(gè)個(gè)體與的取值所對(duì)應(yīng)的謂詞真值的關(guān)系為與關(guān)系，也就是說(shuō)在個(gè)體域中所有的特定點(diǎn)同時(shí)解釋該謂詞公式。12/30/202227謂詞公式的解釋*用某個(gè)解釋解釋一個(gè)謂詞公式，就是將解釋中的各5.1.2謂詞公式（11）*例：設(shè)個(gè)體域D＝{1,2},求公式A＝xyP(x，y)在D上的解釋?zhuān)⒅赋鲈诿恳环N解釋下公式A的真值。解：公式里沒(méi)有個(gè)體常量和函數(shù)，所以直接為謂詞指派真值，設(shè)為P（1，1）＝TP（1，2）＝FP（2，1）＝TP（2，2）＝F

這就是A在D上的一個(gè)解釋。在此解釋下：當(dāng)x＝1時(shí)有y＝1使P（x，y）的真值為T(mén)；當(dāng)x＝2時(shí)有y＝1使P（x，y）的真值為T(mén)；即對(duì)于D中的所有X都有y＝1使P（x，y）的真值為T(mén)，所以在此解釋下公式A的真值為T(mén)。12/30/2022285.1.2謂詞公式（11）*例：設(shè)個(gè)體域D＝{1,2},求補(bǔ)充前題設(shè)個(gè)體域D＝{1,2},求公式A＝xyP(x，y)在D上的解釋?zhuān)⒅赋鲈诿恳环N解釋下公式A的真值。xyP(x，y)=>(P(1,1)∨P(1,2))∧(P(2,1)∨P(2,2))取P(1,1)=T,P(1,2)=T,P(2,1)=F,P(2,2)=F時(shí),A的真值為F。取P(1,1)=T,P(1,2)=F,P(2,1)=F,P(2,2)=T時(shí),A的真值為T(mén)。12/30/202229補(bǔ)充前題設(shè)個(gè)體域D＝{1,2},求公式A＝xyP(x，y5.1.2謂詞公式（12）*例：設(shè)個(gè)體域D＝{1,2},求公式B＝xP（x）Q（f(x),b）在D上的解釋?zhuān)⒅赋鲈诿恳环N解釋下公式B的真值。解：為個(gè)體常量b指派D中的值：b=1為函數(shù)f(x)指派D中的值:f(1)=2,f(2)=1對(duì)謂詞指派真值為：P(1)=F,P(2)=T,Q(1,1)=T,Q(2,1)=F

在此解釋下，當(dāng)x＝1時(shí)：P(1)=F,Q(f(1),1)=Q(2,1)=F所以P（x）Q（f(x),b）為T(mén)。當(dāng)x＝2時(shí)有:P(2)=T,Q(f(2),1)=Q(1,1)=T所以P（x）Q（f(x),b）為T(mén)。即對(duì)個(gè)體域D中的所有x均有P（x）Q（f(x),b），所以公式B在此解釋下的真值為T(mén)。12/30/2022305.1.2謂詞公式（12）*例：設(shè)個(gè)體域D＝{1,2},5.1.2謂詞公式（14）定義6：謂詞公式在個(gè)體域上的永真、永假、可滿足設(shè)P為謂詞公式，D為其個(gè)體域，對(duì)于D中的任一解釋I：（1）若P恒為真，則稱(chēng)P在D上永真或是D上的永真式。（2）若P恒為假，則稱(chēng)P在D上永假或是D上的永假式。（3）若至少有一個(gè)解釋?zhuān)墒筆為真，則稱(chēng)P在D上是可滿足式。12/30/2022315.1.2謂詞公式（14）定義6：謂詞公式在個(gè)體域上的永真5.1.2謂詞公式（15）定義7：謂詞公式全個(gè)體域上的永真、永假、可滿足設(shè)P為謂詞公式，對(duì)于任何個(gè)體域：（1）若P都永真，則稱(chēng)P為永真式。（2）若P都永假，則稱(chēng)P為永假式。（3）若P都可滿足，則稱(chēng)P為可滿足式。謂詞公式的真值與個(gè)體域及解釋有關(guān)，考慮到個(gè)體域的數(shù)目和個(gè)體域中元素?cái)?shù)目無(wú)限的情形，所以要通過(guò)算法判斷一個(gè)謂詞公式永真是不可能的，所以稱(chēng)一階謂詞邏輯是不可判定的（半可判定）。12/30/2022325.1.2謂詞公式（15）定義7：謂詞公式全個(gè)體域上的永真5.1.3謂詞邏輯中的形式演繹推理（1）自然演繹推理

利用一階謂詞推理規(guī)則的符號(hào)表示形式，可以把關(guān)于自然語(yǔ)言的邏輯推理問(wèn)題，轉(zhuǎn)化為符號(hào)表達(dá)式的推演變換。這種推理十分類(lèi)似于人們用自然語(yǔ)言推理的思維過(guò)程，因而稱(chēng)為自然演繹推理。在推理過(guò)程中常用到的推理規(guī)則的符號(hào)表示形式：常用邏輯等價(jià)式常用邏輯蘊(yùn)含式

12/30/2022335.1.3謂詞邏輯中的形式演繹推理（1）自然演繹推理12/常用邏輯等價(jià)式（1）12/30/202234常用邏輯等價(jià)式（1）12/29/202234常用邏輯等價(jià)式（2）12/30/202235常用邏輯等價(jià)式（2）12/29/202235常用邏輯等價(jià)式（3）12/30/202236常用邏輯等價(jià)式（3）12/29/202236常用邏輯等價(jià)式（4）12/30/202237常用邏輯等價(jià)式（4）12/29/202237常用邏輯蘊(yùn)含式（1)12/30/202238常用邏輯蘊(yùn)含式（1)12/29/202238常用邏輯蘊(yùn)含式(2)12/30/202239常用邏輯蘊(yùn)含式(2)12/29/2022395.1.3謂詞邏輯中的形式演繹推理（2）例5.4設(shè)有前提：（1）凡是大學(xué)生都學(xué)過(guò)計(jì)算機(jī)；（2）小王是大學(xué)生。試問(wèn)：小王學(xué)過(guò)計(jì)算機(jī)嗎？解：令S（x）：x是大學(xué)生M（x）：x學(xué)過(guò)計(jì)算機(jī)；a：小王上面命題用謂詞公式表示為：[前提][(1),US][前提][(2),(3),I3]我們進(jìn)行形式推理：M(a)，即小王學(xué)過(guò)計(jì)算機(jī)。xA(x)=>A(y)y是個(gè)體域中任一確定元素(AB)A=>B,假言推理12/30/2022405.1.3謂詞邏輯中的形式演繹推理（2）例5.4設(shè)有前5.1.3謂詞邏輯中的形式演繹推理（3）例5.5證明是和的邏輯結(jié)果。證：[前提][(1),US][(2),US][前提][(3),(4),I4](AB)?B=>?A拒取式得證12/30/2022415.1.3謂詞邏輯中的形式演繹推理（3）例5.5證明5.1.3謂詞邏輯中的形式演繹推理（4）例5.6證明

證：[前提][(1),US][(2),E24][(3),(5),I6][前提][(4),US][(6),UG]AB=>?B?A逆反律(AB)(BC)=>AC假言三段論A(y)=>xA(x)

全稱(chēng)推廣規(guī)則得證12/30/2022425.1.3謂詞邏輯中的形式演繹推理（4）例5.6證明證：一階謂詞邏輯的特點(diǎn)優(yōu)點(diǎn)

（1）自然性

謂詞邏輯是一種接近于自然語(yǔ)言的形式語(yǔ)言，用它表示的知識(shí)比較容易理解；（2）精確性

謂詞邏輯是二值邏輯，其謂詞公式的真值只有“真”與“假”兩個(gè)，因此可以用它表示精確的知識(shí)。（3）容易實(shí)現(xiàn)

用謂詞邏輯表示的知識(shí)可以容易地轉(zhuǎn)換為計(jì)算機(jī)的內(nèi)部形式，分析過(guò)程容易在計(jì)算機(jī)上實(shí)現(xiàn)。缺點(diǎn)（1）效率低

用謂詞邏輯表示知識(shí)時(shí)，把推導(dǎo)與知識(shí)的語(yǔ)義分開(kāi)，使得推理過(guò)程變長(zhǎng)，推理規(guī)則太多，中間結(jié)論呈指數(shù)增長(zhǎng)，實(shí)施困難。（2）靈活性差

謂詞邏輯表示法只能表示精確的知識(shí)，不能表示不精確的知識(shí)，而人類(lèi)的知識(shí)中有許多不精確或是模糊的知識(shí)，使得表示知識(shí)的范圍受到了限制。12/30/202243一階謂詞邏輯的特點(diǎn)優(yōu)點(diǎn)

12/29/2022435.2歸結(jié)演繹推理5.2.1子句集5.2.2命題邏輯中的歸結(jié)原理5.2.3替換與合一5.2.4謂詞邏輯中的歸結(jié)原理12/30/2022445.2歸結(jié)演繹推理5.2.1子句集12/29/202245.2.1子句集(1)定義1：原子謂詞公式及其否定稱(chēng)為文字若干個(gè)文字的一個(gè)析取式稱(chēng)為一個(gè)子句由r個(gè)文字組成的子句叫r-文字子句1-文字子句叫單元子句不含任何文字的子句稱(chēng)為空子句，記為□或NIL。例如：?D(y)I(a)

PQ?R

?I(z)R(z)12/30/2022455.2.1子句集(1)定義1：原子謂詞公式及其否定稱(chēng)為文字例5.2.1子句集(2)謂詞公式例

x{yP(x,y)?y[Q(x,y)R(x,y)]}子句集例

{?P(x,f(x))Q(x,g(x)),?P(y,f(y))?R(y,g(y))}謂詞公式與子句集有哪些區(qū)別？“?”作用原子謂詞沒(méi)有量詞(、)合取范式元素之間變?cè)煌x2：對(duì)一個(gè)謂詞公式G，通過(guò)以下步驟所得的子句集S，稱(chēng)為G的子句集（clauses）。

集合形式?jīng)]有蘊(yùn)含詞、等值詞12/30/2022465.2.1子句集(2)謂詞公式例謂詞公式與子句集有哪些區(qū)別？5.2.1子句集(3)例5.7：x{yP(x，y)?y[Q(x,y)R(x,y)]}由第一步可得：x{?yP(x，y)?y[?Q(x,y)R(x,y)]}1、消蘊(yùn)含詞和等值詞

理論根據(jù)：AB?ABAB(?AB)(?BA)蘊(yùn)含等價(jià)式問(wèn)題:蘊(yùn)含式y(tǒng)P(x，y)?y[Q(x,y)R(x,y)]的前件是？1：yP(x，y)2：P(x，y)

12/30/2022475.2.1子句集(3)例5.7：x{yP(x，y5.2.1子句集(4)“?”作用原子謂詞沒(méi)有量詞(、)合取范式元素之間變?cè)煌闲问經(jīng)]有蘊(yùn)含詞、等值詞12/30/2022485.2.1子句集(4)“?”作用原子謂詞沒(méi)有量詞(、5.2.1子句集(5)x{?yP(x，y)?y[?Q(x,y)R(x,y)]}

2、移動(dòng)否定詞作用范圍，使其僅作用于原子公式

理論根據(jù)：?(?A)A?(AB)?A?B ?(AB)?A?B ?xP(x)x?P(x) ?xP(x)x?P

(x)雙重否定律摩根定律量詞轉(zhuǎn)換定律=>x{y?P(x，y)y?[?Q(x,y)R(x,y)]}

=>

x{y?P(x，y)y[?(?

Q(x,y))?R(x,y)]}=>

x{y?P(x，y)y[Q(x,y)?R(x,y)]}12/30/2022495.2.1子句集(5)x{?yP(x，y)5.2.1子句集(6)“?”作用原子謂詞沒(méi)有量詞(、)合取范式元素之間變?cè)煌闲问經(jīng)]有蘊(yùn)含詞、等值詞12/30/2022505.2.1子句集(6)“?”作用原子謂詞沒(méi)有量詞(、5.2.1子句集(7)=>x{y?P(x，y)z[Q(x,z)?R(x,z)]}3、適當(dāng)改名，使變量標(biāo)準(zhǔn)化即：對(duì)于不同的約束，對(duì)應(yīng)于不同的變量x{y?P(x，y)y[Q(x,y)?R(x,y)]}問(wèn)題:不同轄域的相同變?cè)獙?duì)應(yīng)的約束相同嗎?12/30/2022515.2.1子句集(7)=>x{y?P(x，y)5.2.1子句集(8)4、

消去存在量詞(Skolem化）,同時(shí)進(jìn)行變?cè)鎿Q

原則：

①若該存在量詞不在任何全稱(chēng)量詞的轄域內(nèi)，則用一個(gè)常量符號(hào)代替該存在量詞轄域內(nèi)的相應(yīng)約束變?cè)?/p>

這個(gè)常量叫Skolem常量；②若該存在量詞在全稱(chēng)量詞的轄域內(nèi)，則用這些全稱(chēng)量詞指導(dǎo)變?cè)囊粋€(gè)函數(shù)代替該存在量詞轄域內(nèi)的相應(yīng)約束變?cè)?，這樣的函數(shù)稱(chēng)為Skolem函數(shù)。理論依據(jù)：

xA（x）=>A（y）y是個(gè)體域中某一確定的元素。

存在指定規(guī)則12/30/2022525.2.1子句集(8)4、消去存在量詞(Skolem化）5.2.1子句集(9)問(wèn)題:為什么受全稱(chēng)量詞約束的要用Skolem函數(shù)替換?而不能用常量替換？xyM（y，x）：對(duì)任意一個(gè)人x，都存在一個(gè)y，y是x的媽媽。若去掉存在量詞用常量a代替y，則變?yōu)椋簒M（a，x）：a是所有人的媽媽。實(shí)際上，引入Skolem函數(shù)，是由于存在量詞在全稱(chēng)量詞的轄域之內(nèi)，其約束變?cè)娜≈低耆蕾囉谌Q(chēng)變量的取值。而Skolem函數(shù)反映了這種依賴關(guān)系。12/30/2022535.2.1子句集(9)問(wèn)題:為什么受全稱(chēng)量詞約束的要用Sko5.2.1子句集(10)x{y?P(x，y)z[Q(x,z)?R(x,z)]}=>x{?P(x，f(x))[Q(x，g(x))?R(x，g(x))]}=>

?P(x，f(x))[Q(x,g(x))?R(x,g(x))]5、消去所有全稱(chēng)量詞。理論依據(jù)：

xA（x）=>A（y）y是個(gè)體域中任一確定的元素。

全稱(chēng)指定規(guī)則12/30/2022545.2.1子句集(10)x{y?P(x，y)5.2.1子句集(11)子句集的特征“?”作用原子謂詞沒(méi)有量詞(、)合取范式元素之間變?cè)煌闲问經(jīng)]有蘊(yùn)含詞、等值詞12/30/2022555.2.1子句集(11)子句集的特征“?”作用原子謂詞沒(méi)有量5.2.1子句集(12)=>[?P(x，f(x))Q(x,g(x))][?P(x，f(x))?R(x,g(x))]6、化公式為合取范式理論依據(jù)：A（BC）（AB）（AC）（AB）C（AC）（BC）?P(x，f(x))[Q(x,g(x))?R(x,g(x))]

分配律12/30/2022565.2.1子句集(12)=>[?P(x，f(x))5.2.1子句集(13)子句集的特征“?”作用原子謂詞沒(méi)有量詞(、)合取范式元素之間變?cè)煌闲问經(jīng)]有蘊(yùn)含詞、等值詞12/30/2022575.2.1子句集(13)子句集的特征“?”作用原子謂詞沒(méi)有量5.2.1子句集(14)=>[?P(x，f(x))Q(x,g(x))][?P(y，f(y))?R(y,g(y))]7、適當(dāng)改名，使子句間無(wú)同名變?cè)?>{?P(x，f(x))Q(x,g(x)),?P(y，f(y))?R(y,g(y))}8、消去合取詞，以子句為元素組成一個(gè)集合S=>

?P(x，f(x))[Q(x,g(x))?R(x,g(x))]12/30/2022585.2.1子句集(14)=>[?P(x，f(x))Q5.2.1子句集-小結(jié)消去蘊(yùn)含詞和等值詞使否定詞僅作用于原子公式使量詞間不含同名指導(dǎo)變?cè)ゴ嬖诹吭~消去全稱(chēng)量詞化公式為合取范式子句間無(wú)同名變?cè)M成一個(gè)集合“?”作用原子謂詞沒(méi)有量詞(、)合取范式元素之間變?cè)煌闲问經(jīng)]有蘊(yùn)含詞、等值詞蘊(yùn)含等價(jià)式雙重否定律、摩根定律、量詞轉(zhuǎn)換律存在指定、依賴關(guān)系全稱(chēng)指定分配律12/30/2022595.2.1子句集-小結(jié)消去蘊(yùn)含詞和等值詞使否定詞僅作用于原5.2.1子句集-練習(xí)（1）練習(xí)：用謂詞公式表示下述命題。已知前提：（1）自然數(shù)都是大于零的整數(shù)。（2）所有整數(shù)不是偶數(shù)就是奇數(shù)。（3）偶數(shù)除以2是整數(shù)。結(jié)論：所有自然數(shù)不是奇數(shù)就是除以2為整數(shù)的數(shù)?；疐1F2F3

?G的子句集。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)(I(s(x))O(x)))12/30/2022605.2.1子句集-練習(xí)（1）練習(xí)：用謂詞公式表示下述命題。5.2.1子句集-練習(xí)（2）F1:x(N(x)GZ(x)I(x))由(1)得x(?N(x)(GZ(x)I(x)))

x((?N(x)I(x))(?N(x)GZ(x)))由(5)得(?N(x)I(x))(?N(x)GZ(x))由(7)得(?N(x)I(x))(?N(y)GZ(y))由(8)得{?N(x)I(x),?N(y)GZ(y)}

F2:x(I(x)(E(x)O(x)))由(1)得x(?I(x)(E(x)O(x)))由(5)得?I(z)E(z)O(z)由(8)得{?I(z)E(z)O(z)}12/30/2022615.2.1子句集-練習(xí)（2）F1:x(N(x)GZ(5.2.1子句集-練習(xí)（3）F3:x(E(x)I(s(x)))由(1)得x(?E(x)I(s(x)))由(5)得?E(x)I(s(x))由(8)得{?E(u)I(s(u))}?G:?x(N(x)(I(s(x))O(x)))由(1)得?x(?N(x)(I(s(x))O(x)))由(2)得x?(?N(x)(I(s(x))O(x)))

x(N(x)?I(s(x))?O(x))由(4)得N(a)?I(s(a))?O(a)由(8)得{N(a),?I(s(a)),?O(a)}12/30/2022625.2.1子句集-練習(xí)（3）F3:x(E(x)I(s5.2.1子句集-練習(xí)（4）解：F1F2F3?G的子句集為（1）?N(x)GZ(x)（2）?N(y)I(y)（3）?I(z)E(z)O(z)（4）?E(u)I(s(u))（5）N(a)（6）?O(a)（7）?I(s(a))12/30/2022635.2.1子句集-練習(xí)（4）解：F1F2F3?G的子5.2.1子句集-練習(xí)應(yīng)用歸結(jié)原理證明定理（1）?N(x)GZ(x)（2）?N(y)I(y)（3）?I(z)E(z)O(z)（4）?E(u)I(s(u))（5）N(a)（6）?I(s(a))（7）?O(a)（8）?E(a)[4,6,{a/u}]（9）?I(a)E(a)[3,7,{a/z}]（10）?I(a)[8,9]（11）?N(a)[2,10]（12）□[5,11]12/30/2022645.2.1子句集-練習(xí)應(yīng)用歸結(jié)原理證明定理（1）?N(x5.2.1子句集(18)Skolem標(biāo)準(zhǔn)型在求子句集的過(guò)程中，消去存在量詞之后，把所有全稱(chēng)量詞都依次移到式子的最左邊（或者把所有的量詞都依次移到式子最左邊，再消去存在量詞），再將右部的式子化為合取范式，這樣得到的式子就是原公式的Skolem標(biāo)準(zhǔn)型。x{y?P(x,y)z[Q(x,z)?R(x,z)]}=>x{?P(x,f(x))[Q(x,g(x))?R(x,g(x))]}=>x{[?P(x,f(x))Q(x,g(x))][?P(x,f(x))?R(x,g(x))]}{?P(x，f(x))Q(x,g(x)),?P(y，f(y))?R(y,g(y))}消去合取詞和全稱(chēng)量詞，就得到了原公式的子句集12/30/2022655.2.1子句集(18)Skolem標(biāo)準(zhǔn)型在求子句集5.2.1子句集(19)例5.8設(shè)消去存在量詞用a代替x用f(y,z)代替u用g(y,z,v)代替w得到G的Skolem標(biāo)準(zhǔn)型進(jìn)而得G的子句集為：

一個(gè)謂詞公式的子句集也可以通過(guò)求前束范式（如果謂詞公式中一切量詞都位于該公式最左邊，不含否定詞，且量詞的轄域都延伸到公式末端），再求Skolem標(biāo)準(zhǔn)型而得到。12/30/2022665.2.1子句集(19)例5.8設(shè)消去存在量詞進(jìn)而得G的子5.2.1子句集(20)

引入Skolem函數(shù)，是由于存在量詞在全稱(chēng)量詞的轄域內(nèi)，其約束變?cè)娜≈低耆蕾囉谌Q(chēng)量詞的取值。Skolem函數(shù)反映了這種依賴關(guān)系。但Skolem標(biāo)準(zhǔn)型與原公式一般并不等價(jià)。

有公式：G＝xP(x)它的Skolem標(biāo)準(zhǔn)型是G’＝P(a)我們給出如下的解釋I：D＝{0,1},a/0,P(0)/F,P(1)/T在此解釋下，G＝T,G’＝F12/30/2022675.2.1子句集(20)引入Skolem函數(shù)，是由5.2.1子句集(21)定理1：謂詞公式G不可滿足當(dāng)且僅當(dāng)其子句集S不可滿足定義3：子句集S是不可滿足的，當(dāng)且僅當(dāng)其全部子句的合取式是不可滿足的。謂詞公式正確性證明謂詞公式否定式不可滿足性證明謂詞公式對(duì)應(yīng)子句集的不可滿足性證明12/30/2022685.2.1子句集(21)定理1：謂詞公式G不可滿足當(dāng)且僅當(dāng)5.2.2命題邏輯中的歸結(jié)原理(1)歸結(jié)原理的提出歸結(jié)原理(principleofresolution)又稱(chēng)消解原理,1965年魯濱遜（J.A.Robinson）提出，從理論上解決了定理證明問(wèn)題。歸結(jié)原理提出的是一種證明子句集不可滿足性，從而實(shí)現(xiàn)定理證明的一種理論及方法。歸結(jié)原理的基本原理是采用反證法（反演推理方法）歸結(jié)算法是一節(jié)謂詞邏輯中的半可判定算法，對(duì)一階邏輯中任意恒真公式使用歸結(jié)原理，總可以在有限步內(nèi)給以判定（證明其為永真）對(duì)不知該公式是否為恒真時(shí)，使用歸結(jié)原理得不到任何結(jié)論12/30/2022695.2.2命題邏輯中的歸結(jié)原理(1)歸結(jié)原理的提出12/25.2.2命題邏輯中的歸結(jié)原理(2)定義4設(shè)L為一個(gè)文字，則L與?L為互補(bǔ)文字。

定義5設(shè)C1、C2是命題邏輯中的兩個(gè)子句，C1中有文字L1、C2中有文字L2、且L1與L2互補(bǔ)，從C1、C2中分別刪除L1、L2，再將剩余部分析取起來(lái)，構(gòu)成的新子句為C12，則C12為C1、C2的

歸結(jié)式，C1、C2稱(chēng)為其歸結(jié)式的親本子句，稱(chēng)L1、L2為消解基。例5.9設(shè)，則C1、

C2的歸結(jié)式為：

12/30/2022705.2.2命題邏輯中的歸結(jié)原理(2)定義4設(shè)L為一個(gè)文5.2.2命題邏輯中的歸結(jié)原理(3)定理2歸結(jié)式是其親本子句的邏輯結(jié)果。證明：設(shè)C1=LC1’，C2=?LC2’其中C1’、C2’都是文字的析取式。

C1、C2的歸結(jié)式為C1’C2’

C1、C2的邏輯結(jié)果為：

C1=C1’L=?C1’→

LC2=?LC2’=L→C2’由假言三段論可得：

C1∧

C2=（?C1’→L）∧（L→C2’）=>?C1’→

C2’=C1’C2’命題邏輯中的歸結(jié)原理：12/30/2022715.2.2命題邏輯中的歸結(jié)原理(3)定理2歸結(jié)式5.2.2命題邏輯中的歸結(jié)原理(4)例5.10用歸結(jié)原理驗(yàn)證分離規(guī)則和拒取式

A∧(A→B)＝＞B(A→B)∧﹁B＝＞﹁A

解

A∧(A→B)＝A∧(﹁A∨B)＝＞B(A→B)∧﹁B＝(﹁A∨B)∧(﹁B)＝＞﹁A

12/30/2022725.2.2命題邏輯中的歸結(jié)原理(4)例5.10用歸結(jié)原5.2.2命題邏輯中的歸結(jié)原理(5)類(lèi)似的可以驗(yàn)證其他推理規(guī)則。這說(shuō)明，歸結(jié)原理可以代替其他所有的推理規(guī)則，而且推理步驟比較機(jī)械，為機(jī)器推理提供了方便。由歸結(jié)原理可知：L∧?L＝NIL另外我們知道：L∧?L＝F（假），也就是

NILF空子句就是恒假子句12/30/2022735.2.2命題邏輯中的歸結(jié)原理(5)類(lèi)似的可以驗(yàn)證其他推理補(bǔ)充：定理1G為F1,F2,…，F(xiàn)n的邏輯結(jié)論，當(dāng)且僅當(dāng)（F1F2…Fn）=>G定理2G為F1,F2,…，F(xiàn)n的邏輯結(jié)論，當(dāng)且僅當(dāng)(F1F2…Fn)﹁G是不可滿足的。12/30/202274補(bǔ)充：定理1G為F1,F2,…，F(xiàn)n的邏輯結(jié)論，當(dāng)且5.2.2命題邏輯中的歸結(jié)原理(6)利用歸結(jié)原理證明命題公式的思路先求出要證明的命題公式的否定式的子句集S；然后對(duì)子句集S（一次或者多次）使用歸結(jié)原理；若在某一步推出了空子句，即推出了矛盾，則說(shuō)明子句集S是不可滿足的，從而原否定式也是不可滿足的，進(jìn)而說(shuō)明原公式是永真的。12/30/2022755.2.2命題邏輯中的歸結(jié)原理(6)利用歸結(jié)原理證明命題公5.2.2命題邏輯中的歸結(jié)原理(7)推出空子句就說(shuō)明子句集不可滿足，原因是：空子句就是F，推出空子句就是推出了F。歸結(jié)原理是正確的推理形式，由正確的推理形式推出了F，則說(shuō)明前提不真，即歸結(jié)出空子句的兩個(gè)親本子句至少有一個(gè)為假。如果這兩個(gè)親本子句都是原子句集S中的子句，即說(shuō)明原子句集S不可滿足。（因子句間為合取關(guān)系）如果這兩個(gè)親本子句不是或不全是S中的子句，那么它們必定是某次歸結(jié)的結(jié)果。同樣的道理向上回溯，一定會(huì)推出原子句集中至少有一個(gè)子句為假，從而說(shuō)明S不可滿足。12/30/2022765.2.2命題邏輯中的歸結(jié)原理(7)推出空子句就說(shuō)明子句集不5.2.2命題邏輯中的歸結(jié)原理(8)推論設(shè)C1、C2是子句集S的兩個(gè)子句，C12是它們的歸結(jié)式，則（1）若用C12來(lái)代替C1、C2，得到新的子句集S1，則由S1不可滿足性可以推出原子句集S的不可滿足性。即（2）若用C12加入到S中，得到新的子句集S2，則S2與原S的同不可滿足。即S1的不可滿足性=>S不可滿足S2的不可滿足性<=>S不可滿足12/30/2022775.2.2命題邏輯中的歸結(jié)原理(8)推論設(shè)C1、C2是子5.2.2命題邏輯中的歸結(jié)原理(9)例5.12設(shè)公理集：P,(PQ)R,(SU)Q,U求證：R化子句集： (PQ)R=>?(PQ)R=>?P?QR (SU)Q=>?(SU)Q=>(?S?U)Q=>(?SQ)(?UQ)=>{?SQ,?UQ}子句集： (1)P (2)?P?QR (3)?SQ (4)?UQ (5)U (6)?R（目標(biāo)求反）

12/30/2022785.2.2命題邏輯中的歸結(jié)原理(9)例5.12設(shè)公理集：5.2.2命題邏輯中的歸結(jié)原理(10)子句集： (1)P (2)?P?QR (3)?SQ (4)?TQ (5)T (6)?R（目標(biāo)求反）歸結(jié)： (7)?P?Q(2,6) (8)?Q (1,7)(9)?T(4,8)(10)NIL(5,9)?P?QR?R?P?QP?Q?TQ?TTNIL12/30/2022795.2.2命題邏輯中的歸結(jié)原理(10)子句集：歸結(jié)：?P5.2.2命題邏輯中的歸結(jié)原理(11)例5.11證明子句集{P?Q,?P,Q}是不可滿足。證明：子句集： (1)P?Q (2)?P (3)Q歸結(jié)： (4)?Q由（1）和（2） (5)NIL由（4）和（5）得證12/30/2022805.2.2命題邏輯中的歸結(jié)原理(11)例5.11證明子句5.2.3替換與合一(1)問(wèn)題

在一階謂詞中應(yīng)用消解原理，因?yàn)橹^詞邏輯中的子句含有個(gè)體變?cè)?，所以可能無(wú)法直接找到互否文字的子句對(duì)例如：P(x)Q(z),?P(f(y))R(y)

P(x)Q(y),?P(a)R(z)解決方法

對(duì)個(gè)體變?cè)鲞m當(dāng)替換例如：P(f(y))Q(z),?P(f(y))R(y)

P(a)Q(y),?P(a)R(z)12/30/2022815.2.3替換與合一(1)問(wèn)題12/29/2022815.2.3替換與合一(2)定義6一個(gè)替換（Substitution）是形如{t1/x1,t2/x2,…,tn/xn}的有限集合，其中t1,t2,…,tn是項(xiàng)，稱(chēng)為替換的分子；x1,x2,…,xn是互不相同的個(gè)體變?cè)?，稱(chēng)為替換的分母；ti,xi不同，xi不循環(huán)出現(xiàn)在tj中；(i,j=1,2,…,n)ti/xi表示用ti替換xi。若其中t1,t2,…,tn是不含變?cè)捻?xiàng)（稱(chēng)為基項(xiàng)）時(shí)，該替換為基替換；沒(méi)有元素的替換稱(chēng)為空替換，記作ε，表示不作任何替換。例：{a/x,g(a)/y,f(g(b))/z}{g(y)/x,f(x)/y}是一個(gè)替換不是一個(gè)替換，x與y出現(xiàn)了循環(huán)替換12/30/2022825.2.3替換與合一(2)定義6一個(gè)替換（Substit回顧定義項(xiàng)（1）個(gè)體常元和變?cè)际琼?xiàng)。（2）f是n元函數(shù)符號(hào)，若t1,t2,…,tn是項(xiàng)，則f(t1,t2,…,tn)是項(xiàng)。（3）只有有限次使用(1),(2)得到的符號(hào)串才是項(xiàng)原子公式：設(shè)P是n元謂詞符號(hào)，t1,t2,..,tn是項(xiàng),則P(t1,t2,..,tn)是原子謂詞公式文字：原子謂詞公式及其否定式子句：若干文字的析取稱(chēng)為一個(gè)子句12/30/202283回顧定義項(xiàng)12/29/2022835.2.3替換與合一(3)

表達(dá)式：項(xiàng)、原子公式、文字、子句的統(tǒng)稱(chēng)。基表達(dá)式：沒(méi)有變?cè)谋磉_(dá)式。子表達(dá)式：出現(xiàn)在表達(dá)式E中的表達(dá)式稱(chēng)為E的子表達(dá)式。定義7設(shè)θ={t1/x1,t2/x2,…,tn/xn}是一個(gè)替換，E是一個(gè)表達(dá)式，對(duì)E實(shí)施替換θ，即把E中出現(xiàn)的個(gè)體變?cè)獂j都用tj替換，記為Eθ,所得的結(jié)果稱(chēng)為E在θ下的例（instance）。例如：若θ={a/x,f(b)/y,c/z},G=P(x,y,z)

Gθ=P(a,f(b),c)12/30/2022845.2.3替換與合一(3)表達(dá)式：項(xiàng)、原子公式、文字、子5.2.3替換與合一(4)定義8設(shè)θ＝{t1/x1,t2/x2,…,tm/xm}，λ＝{u1/y1,u2/y2,…,un/yn}是兩個(gè)替換，則將{t1λ/x1,t2λ/x2,…,tmλ/xm,u1/y1,u2/y2,…,un/yn}中符合下列條件的元素刪除

（1）tiλ

/xi當(dāng)tiλ

＝

xi

（2）ui/yi當(dāng)yi∈

{x1,…,xm}這樣得到的集合為θ與λ的復(fù)合或乘積，記為θ?λ。例：設(shè)θ={f(y)/x,z/y},λ={a/x,b/y,y/z}θ?λ={t1λ

/x1,t2λ

/x2,u1/y1,u2/y2,u3/yn}={f(b)/x，y/y，a/x，b/y，y/z}從而θ

?λ={f(b)/x，y/z}12/30/2022855.2.3替換與合一(4)定義8設(shè)θ＝{t1/x1,5.2.3替換與合一(5)定義9設(shè)S＝{F1,F2,…,Fn}

是一個(gè)原子謂詞公式集，若存在一個(gè)替換θ，可使F1θ

=F2θ=…=Fnθ，則稱(chēng)θ為S的一個(gè)合一，稱(chēng)S為可合一的。例：S={P(x,f(y),b),P(z,f(b),b)}替換θ={a/x,b/y,a/z}是S的一個(gè)合一,因?yàn)椋?P(x,f(y),b)θ=P(a,f(b),b) P(z,f(b),b)θ=P(a,f(b),b)替換θ={z/x,b/y}和替換θ={x/z,b/y}也是S的一個(gè)合一。一個(gè)公式的合一一般不唯一12/30/2022865.2.3替換與合一(5)定義9設(shè)S＝{F1,F2,…5.2.3替換與合一(6)定義10設(shè)σ是原子公式集S的一個(gè)合一，如果對(duì)S的任何一個(gè)合一θ都存在一個(gè)替換λ，使得

θ＝σ?λ則稱(chēng)σ為S的最一般合一(MostGeneralUnifier),簡(jiǎn)稱(chēng)MGU。一個(gè)公式集的MGU也是不唯一的。例：設(shè)S＝{P(u,y,g(y)),P(x,f(u),z)},S有一個(gè)最一般合一

σ＝{u/x，f(u)/y，g(f(u))/z}對(duì)S的任一合一，例如：

θ＝{a/x，f(a)/y，g(f(a))/z，a/u}存在一個(gè)替換

λ＝{a/u}使得θ＝σ

?λ12/30/2022875.2.3替換與合一(6)定義10設(shè)σ是原子公式集S的一5.2.3替換與合一(7)定義11設(shè)S是一個(gè)非空的具有相同謂詞名的原子公式集，從S中各公式左邊的第一項(xiàng)開(kāi)始，同時(shí)向右比較，直到發(fā)現(xiàn)第一個(gè)不都相同的項(xiàng)為止，用這些項(xiàng)的差異部分組成的集合就是S的一個(gè)差異集。例：設(shè)S＝{P(x,y,z),P(x,f(a),h(b))}根據(jù)上述差異集定義可以看出S有兩個(gè)差異集：D1＝{y,f(a)}D2＝{z,h(b)}12/30/2022885.2.3替換與合一(7)定義11設(shè)S是一個(gè)非空的具有相5.2.3替換與合一(8)合一算法（Unificationalgorithm）Step1：置k＝0，Sk＝S，σk＝ε；Step2：若Sk只含有一個(gè)謂詞公式，則算法停止，σk就是最一般合一；Step3：求Sk的差異集Dk；Step4：若Dk中存在元素xk和tk，其中xk是變?cè)瑃k是項(xiàng)且xk不在tk中出現(xiàn)，則置Sk＋1＝Sk{tk/

xk}，σk+1=σk?{tk/xk}

，k＝k+1，然后轉(zhuǎn)Step2；Step5：算法停止，S的最一般合一不存在。12/30/2022895.2.3替換與合一(8)合一算法（Unification5.2.3替換與合一(9)例：求公式集S＝{P(a,x,f(g(y))),P(z,h(z,u),f(u))}的最一般合一。解k＝0；S0＝S，σ0＝ε，求得D0＝{a,z}σ1＝σ0·{a/z}={a/z}S1=S0{a/z}={P(a,x,f(g(y))),P(a,h(a,u),f(u))}k＝1；求得D1={x,h(a,u)}σ2=σ1·{h(a,u)/x}＝{a/z,h(a,u)/x}S2=S1{h(a,u)/x}={P(a,h(a,u),f(g(y))),P(a,h(a,u),f(u))}k＝2；求得D2＝{g(y),u}σ3＝{a/z,h(a,g(y))/x,g(y)/u}S3=S2{g(y)/u}={P(a,h(a,g(y)),f(g(y)))}S3是單元素集，σ3為MGU。12/30/2022905.2.3替換與合一(9)例：求公式集S＝{P(a,x,f5.2.3替換與合一(10)例5.17判定S=｛P(x,x),P(y,f(y))｝是否可合一？解k=0:S0=S,σ0=ε,S0不是單元素集，D0=｛x,y｝σ1=σ0·｛y/x｝=｛y/x｝S1=S0｛y/x｝=｛P(y,y),P(y,f(y))｝k=1:

S1不是單元素集，D1=｛y,f(y)｝，由于變?cè)獃在項(xiàng)f(y)中出現(xiàn)，所以算法停止，S不存在最一般合一。

12/30/2022915.2.3替換與合一(10)例5.17判定S=｛P(x,5.2.3替換與合一(11)定理3(合一定理)S是非空有限可合一的公式集，則合一算法總在Step2停止，且最后的σk即是S的最一般合一（MGU）。對(duì)任一非空有限可合一的公式集，一定存在最一般合一，而且用合一算法一定能找到最一般合一，即算法終止在第2步時(shí)最后的合一σk從合一算法可以看出，一個(gè)公式集S的最一般合一可能是不唯一的。如果差異集Dk=｛ak,bk｝，且ak和bk都是個(gè)體變?cè)瑒t下面兩種選擇都是合適的：σk+1=σk·｛bk/ak｝或σk+1=σk·｛ak/bk｝12/30/2022925.2.3替換與合一(11)定理3(合一定理)S是非5.2.4謂詞邏輯中的歸結(jié)原理(1)例：P(x)Q(y),?P(f(z))R(z) =>Q(y)R(z)定義12設(shè)C1，C2為無(wú)相同變?cè)淖泳洌籐1，L2為其中的兩個(gè)文字;L1和?L2有最一般合一σ；則C1，C2的二元?dú)w結(jié)式（二元消解式）為：

（C1σ－{L1σ}）∪（C2σ－{L2σ}）其中C1，C2稱(chēng)作歸結(jié)式的親本子句；L1，L2稱(chēng)作消解文字。

12/30/2022935.2.4謂詞邏輯中的歸結(jié)原理(1)例：P(x)Q(y5.2.4謂詞邏輯中的歸結(jié)原理(2)例5.18設(shè)C1=P(x)∨Q(x),C2=?P(a)∨R(y)，求C1,C2的歸結(jié)式。解取L1=P(x),?L2=P(a),L1與?L2的MGUσ={a/x｝(C1σ-｛L1σ｝)∪(C2σ-｛L2σ｝)=({P(a),Q(a)}-{P(a)})∪({?P(a),R(y)}-{?P(a)})

={Q(a),R(y)}=Q(a)∨R(y)所以，Q(a)∨R(y)是C1和C2的二元?dú)w結(jié)式。12/30/2022945.2.4謂詞邏輯中的歸結(jié)原理(2)例5.18設(shè)C1=5.2.4謂詞邏輯中的歸結(jié)原理(3)

例5.19設(shè)C1=P(x,y)∨Q(a),C2=?Q(x)∨R(y),求C1,C2的歸結(jié)式。解由于C1,C2中都含有變?cè)獂,y，所以需先對(duì)其中一個(gè)進(jìn)行改名,方可歸結(jié)。2、如果在參加歸結(jié)的子句內(nèi)部含有可合一的文字，則在進(jìn)行歸結(jié)之前，也應(yīng)對(duì)這些文字進(jìn)行合一，從而使子句達(dá)到最簡(jiǎn)。歸結(jié)過(guò)程需要注意兩點(diǎn)：1、兩個(gè)子句含有相同的變?cè)枰獙?duì)其中一個(gè)進(jìn)行改名12/30/2022955.2.4謂詞邏輯中的歸結(jié)原理(3)例5.19設(shè)C1=P5.2.4謂詞邏輯中的歸結(jié)原理(4)例如，設(shè)有兩個(gè)子句：C1=P(x)∨P(f(a))∨Q(x)C2=?P(y)∨R(b)可見(jiàn),在C1中有可合一的文字P(x)與P(f(a))取替換θ={f(a)/x}現(xiàn)在再用C1θ與C2進(jìn)行歸結(jié)，從而得到C1與C2的歸結(jié)式Q(f(a))∨R(b)則得C1θ=P(f(a))∨Q(f(a))12/30/2022965.2.4謂詞邏輯中的歸結(jié)原理(4)例如，設(shè)有兩個(gè)子句：可見(jiàn)5.2.4謂詞邏輯中的歸結(jié)原理(5)例5.20：C＝P(x)P(f(y))?Q(x),σ={f(y)/x}

Cσ＝P(f(y))?Q(f(y))是C的因子。定義13子句C中，兩個(gè)或兩個(gè)以上的文字有一個(gè)最一般合一σ，則稱(chēng)Cσ為C的因子，若Cσ為單元子句，則Cσ稱(chēng)為C的單因子。12/30/2022975.2.4謂詞邏輯中的歸結(jié)原理(5)例5.20：C＝P(x5.2.4謂詞邏輯中的歸結(jié)原理(6)定義14子句的C1，C2消解式，是下列二元消解式之一:

（1）C1和C2的二元消解式；（2）C1和C2的因子的二元消解式；（3）C1因子和C2的二元消解式；（4）C1的因子和C2的因子的二元消解式。12/30/2022985.2.4謂詞邏輯中的歸結(jié)原理(6)定義14子句的C1，5.2.4謂詞邏輯中的歸結(jié)原理(7)定理4謂詞邏輯中的消解（歸結(jié)）式是它的親本子句的邏輯結(jié)果。謂詞邏輯的推理規(guī)則（消解原理或歸結(jié)原理）：

C1

C2

＝>（C1

σ－{L1

σ}）∪（

C2σ－{L2σ}）

其中C1、C2是兩個(gè)無(wú)相同變?cè)淖泳?，L1，L2分別是C1，C2中的文字,σ為L(zhǎng)1和?L2的最一般合一。12/30/2022995.2.4謂詞邏輯中的歸結(jié)原理(7)定理4謂詞邏輯中的5.2.4謂詞邏輯中的歸結(jié)原理(8)例5.21求證G是A1和A2的邏輯結(jié)果。A1：(x)(P(x)(Q(