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

6/29/202385.1.1謂詞、函數(shù)、量詞（3）謂詞(predicate)：一般形式為P(x1,x2,…,

xn)其中，P為謂詞名，用于刻畫個體的性質、狀態(tài)或個體間的關系。

x1,x2,…,xn是個體，表示某個獨立存在的事物或者某個抽象的概念。例如：S(x):x是學生；P(x,y):x是y的雙親。個體變元的變化范圍稱為個體域。包攬一切事物的集合稱為全總個體域。6/29/202395.1.1謂詞、函數(shù)、量詞（4）函數(shù)：為了表達個體之間的對應關系，引入數(shù)學中函數(shù)概念和記法。用形如f(x1,x2,…,xn)來表示個體變元對應的個體y，并稱之為n元個體函數(shù)，簡稱函數(shù)。f是函數(shù)符號。函數(shù)增強了謂詞的表達能力函數(shù)father(x):值為x的父親。謂詞Doctor(father(Li)):表示Li的父親是醫(yī)生，值為真或假。符號約定：謂詞符號－大寫字母；P(x,y)函數(shù)符號－小寫字母；f(x)個體變元符號－x、y、z、u、v……個體常元符號－a、b、c…….。P(a,b)6/29/202310邏輯聯(lián)結詞聯(lián)結詞優(yōu)先級應用?否定1?p,非p^合取2p^q,不僅p,而且q、既p,又q、一邊p,一邊q、雖然p,但是q∨析取2相容的或p∨q,排斥的或p∨?q^?p∨q蘊含3p->q，q是p的必要條件，p是q的充分條件。只要p就q、p僅當q、只有q才p<->等價3p<->q，p和q互為充分必要條件P當且僅當q同級從左向右順序演算6/29/2023115.1.1謂詞、函數(shù)、量詞（5）表示“對個體域中所有的（或任一個）個體”。記為x所有、一切、全體、凡是等詞統(tǒng)稱為全稱量詞全稱量詞：表示“在個體域中存在個體”。記為x存在、有些、有的、至少有一個等詞統(tǒ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））

6/29/2023125.1.1謂詞、函數(shù)、量詞（6）用謂詞表示命題時，一般取全總個體域，再采用使用限定謂詞的方法來指出每個個體變元的個體域。(2)對存在量詞，把限定詞作為一個合取項加入。即x(P(x)…)例5.2：對于所有的自然數(shù)，均有x+y>x

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

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

xy（N（x）N（y）G(h(x,y),x)）6/29/2023135.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)))用謂詞表示命題時，形式并不是固定的。6/29/2023145.1.1謂詞、函數(shù)、量詞（8）練習：用謂詞公式表示下述命題。已知前提：（1）自然數(shù)都是大于零的整數(shù)。（2）所有整數(shù)不是偶數(shù)就是奇數(shù)。（3）偶數(shù)除以2是整數(shù)。結論：所有自然數(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。6/29/2023155.1.1謂詞、函數(shù)、量詞（9）將上述各語句翻譯成謂詞公式：（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)))

6/29/2023165.1.2謂詞公式（1）定義1：項（1）個體常元和變元都是項。（2）f是n元函數(shù)符號，若t1，t2，…，tn是項，則f(t1，t2，…，tn)是項。（3）只有有限次使用（1），（2）得到的符號串才是項。用謂詞、量詞及真值連結詞可以表達相當復雜的命題，我們把命題的這種符號表達式稱為謂詞公式。6/29/2023175.1.2謂詞公式（2）定義2：原子公式設P為n元謂詞符號，t1，t2，…，tn為項，P(t1，t2，…，tn)稱為原子謂詞公式，簡稱原子或原子公式。從原子謂詞公式出發(fā)，通過命題聯(lián)結詞和量詞，可以組成復合謂詞公式。6/29/2023185.1.2謂詞公式（3）定義3：謂詞公式（1）原子公式是謂詞公式。（2）若A、B是謂詞公式，則?A，AB，AB，AB，A←→B，xA，xA也是謂詞公式。（3）只有有限步應用（1）（2）生成的公式才是謂詞公式。謂詞公式亦稱為謂詞邏輯中的合適（式）公式，記為Wff。由項的定義，當t1，t2，…，tn全為個體常元時，所得的原子謂詞公式就是原子命題公式（命題符號）。所以全體命題公式也是謂詞公式。

6/29/2023195.1.2謂詞公式（4）轄域：緊接于量詞之后被量詞作用（即說明）的謂詞公式稱為該量詞的轄域。指導變元：量詞后的變元為指導變元。約束變元：在一個量詞轄域中與該量詞的指導變元相同的變元稱為約束變元。自由變元：謂詞公式中除了約束變元之外的變元。

（1）xP(x)（2）y(G(y)D(x,y))（3）xG(x)P(x)指導變元約束變元約束變元約束變元自由變元自由變元6/29/2023205.1.2謂詞公式（5）一個變元在一個公式中既可以約束出現(xiàn)，也可以自由出現(xiàn)，為了避免混淆，通過改名規(guī)則改名：對需要改名的變元，應同時更改該變元在量詞及其轄域中的所有出現(xiàn)。新變元符號必須是量詞轄域內原先沒有的，最好是公式中也未出現(xiàn)過的。xG(x)P(x)改為xG(x)P(y)或yG(y)P(x)6/29/2023215.1.2謂詞公式（6）謂詞公式與命題的區(qū)別與聯(lián)系謂詞公式是命題函數(shù)。一個謂詞公式中所有個體變元被量化（在謂詞前加上量詞），謂詞公式就變成了一個命題。從謂詞公式得到命題的兩種方法：給謂詞中的個體變元代入個體常元；把謂詞中的個體變元全部量化。例：謂詞公式P（x）表示“x是素數(shù)”P（a）

xP（x）,xP（x）都是命題6/29/2023225.1.2謂詞公式（7）一階謂詞：僅個體變元被量化的謂詞。二階謂詞：不僅個體變元被量化，函數(shù)符號和謂詞符號也被量化。如：

P

xP（x）以下兩種命題在個體域為有限集時（n個元素），有下面的等價式全稱命題：

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

特稱命題

xG(x)等價于P(a1)P(a2)…P(an)6/29/2023235.1.2謂詞公式（8）定義4：合取范式（ConjunctiveNormalForm）

設A為如下形式的謂詞公式：B1B2…

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

L2…

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

Q(y))

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

(?Q(x)?R(x,y))就是一個合取范式應用邏輯等價式，任一謂詞公式可化為與之等價的合取范式，一個謂詞的合取范式不唯一6/29/2023245.1.2謂詞公式（9）定義5：析取范式（DisjunctiveNormalForm）設A為如下形式的謂詞公式：B1

B2…

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

L2

…

Lm，Lj（j=1，2,…，m）為原子公式或其否定，則A稱為析取范式。例(P(x)?Q(y)R(x,y))(?P(x)Q(y))(?P(x)R(x,y))就是一個析取范式應用邏輯等價式，任一謂詞公式可化為與之等價的析取范式，一個謂詞的析取范式不唯一6/29/2023255.1.2謂詞公式（10）*謂詞公式的解釋：對謂詞公式中的各種變量指定特殊的常量去替代。設D為謂詞公式P的個體域，若對P中的個體常量、函數(shù)和謂詞按如下規(guī)定賦值：（1）為每個個體常量指派D中的一個元素；（2）為每個n元函數(shù)指派一個從Dn到D的映射，其中Dn＝{(x1,x2,…,xn)|x1,x2,…,xn∈D}（3）為每個n元謂詞指派一個從Dn到{F,T}的映射。稱這些指派(謂詞公式的解釋)為公式P在D上的一個解釋。當被解釋的謂詞公式在特定解釋下真值為真，稱這個解釋滿足這個謂詞公式。6/29/202326謂詞公式的解釋*用某個解釋解釋一個謂詞公式，就是將解釋中的各個值帶到謂詞公式中去，要全部取到。約束出現(xiàn)的變元取值關系與量詞性質有關，當指導變元的相應量詞為存在量詞，此時每個個體域的取值所對應的謂詞真值的關系為或關系，也就是說在個體域中有一個特定點解釋該謂詞公式即可。當指導變元的相應量詞為全稱量詞，此時每個個體與的取值所對應的謂詞真值的關系為與關系，也就是說在個體域中所有的特定點同時解釋該謂詞公式。6/29/2023275.1.2謂詞公式（11）*例：設個體域D＝{1,2},求公式A＝xyP(x，y)在D上的解釋，并指出在每一種解釋下公式A的真值。解：公式里沒有個體常量和函數(shù)，所以直接為謂詞指派真值，設為P（1，1）＝TP（1，2）＝FP（2，1）＝TP（2，2）＝F

這就是A在D上的一個解釋。在此解釋下：當x＝1時有y＝1使P（x，y）的真值為T；當x＝2時有y＝1使P（x，y）的真值為T；即對于D中的所有X都有y＝1使P（x，y）的真值為T，所以在此解釋下公式A的真值為T。6/29/202328補充前題設個體域D＝{1,2},求公式A＝xyP(x，y)在D上的解釋，并指出在每一種解釋下公式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時,A的真值為F。取P(1,1)=T,P(1,2)=F,P(2,1)=F,P(2,2)=T時,A的真值為T。6/29/2023295.1.2謂詞公式（12）*例：設個體域D＝{1,2},求公式B＝xP（x）Q（f(x),b）在D上的解釋，并指出在每一種解釋下公式B的真值。解：為個體常量b指派D中的值：b=1為函數(shù)f(x)指派D中的值:f(1)=2,f(2)=1對謂詞指派真值為：P(1)=F,P(2)=T,Q(1,1)=T,Q(2,1)=F

在此解釋下，當x＝1時：P(1)=F,Q(f(1),1)=Q(2,1)=F所以P（x）Q（f(x),b）為T。當x＝2時有:P(2)=T,Q(f(2),1)=Q(1,1)=T所以P（x）Q（f(x),b）為T。即對個體域D中的所有x均有P（x）Q（f(x),b），所以公式B在此解釋下的真值為T。6/29/2023305.1.2謂詞公式（14）定義6：謂詞公式在個體域上的永真、永假、可滿足設P為謂詞公式，D為其個體域，對于D中的任一解釋I：（1）若P恒為真，則稱P在D上永真或是D上的永真式。（2）若P恒為假，則稱P在D上永假或是D上的永假式。（3）若至少有一個解釋，可使P為真，則稱P在D上是可滿足式。6/29/2023315.1.2謂詞公式（15）定義7：謂詞公式全個體域上的永真、永假、可滿足設P為謂詞公式，對于任何個體域：（1）若P都永真，則稱P為永真式。（2）若P都永假，則稱P為永假式。（3）若P都可滿足，則稱P為可滿足式。謂詞公式的真值與個體域及解釋有關，考慮到個體域的數(shù)目和個體域中元素數(shù)目無限的情形，所以要通過算法判斷一個謂詞公式永真是不可能的，所以稱一階謂詞邏輯是不可判定的（半可判定）。6/29/2023325.1.3謂詞邏輯中的形式演繹推理（1）自然演繹推理

利用一階謂詞推理規(guī)則的符號表示形式，可以把關于自然語言的邏輯推理問題，轉化為符號表達式的推演變換。這種推理十分類似于人們用自然語言推理的思維過程，因而稱為自然演繹推理。在推理過程中常用到的推理規(guī)則的符號表示形式：常用邏輯等價式常用邏輯蘊含式

6/29/202333常用邏輯等價式（1）6/29/202334常用邏輯等價式（2）6/29/202335常用邏輯等價式（3）6/29/202336常用邏輯等價式（4）6/29/202337常用邏輯蘊含式（1)6/29/202338常用邏輯蘊含式(2)6/29/2023395.1.3謂詞邏輯中的形式演繹推理（2）例5.4設有前提：（1）凡是大學生都學過計算機；（2）小王是大學生。試問：小王學過計算機嗎？解：令S（x）：x是大學生M（x）：x學過計算機；a：小王上面命題用謂詞公式表示為：[前提][(1),US][前提][(2),(3),I3]我們進行形式推理：M(a)，即小王學過計算機。xA(x)=>A(y)y是個體域中任一確定元素(AB)A=>B,假言推理6/29/2023405.1.3謂詞邏輯中的形式演繹推理（3）例5.5證明是和的邏輯結果。證：[前提][(1),US][(2),US][前提][(3),(4),I4](AB)?B=>?A拒取式得證6/29/2023415.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)

全稱推廣規(guī)則得證6/29/202342一階謂詞邏輯的特點優(yōu)點

（1）自然性

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

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

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

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

謂詞邏輯表示法只能表示精確的知識，不能表示不精確的知識，而人類的知識中有許多不精確或是模糊的知識，使得表示知識的范圍受到了限制。6/29/2023435.2歸結演繹推理5.2.1子句集5.2.2命題邏輯中的歸結原理5.2.3替換與合一5.2.4謂詞邏輯中的歸結原理6/29/2023445.2.1子句集(1)定義1：原子謂詞公式及其否定稱為文字若干個文字的一個析取式稱為一個子句由r個文字組成的子句叫r-文字子句1-文字子句叫單元子句不含任何文字的子句稱為空子句，記為□或NIL。例如：?D(y)I(a)

PQ?R

?I(z)R(z)6/29/2023455.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ū)別？“?”作用原子謂詞沒有量詞(、)合取范式元素之間變元不同定義2：對一個謂詞公式G，通過以下步驟所得的子句集S，稱為G的子句集（clauses）。

集合形式?jīng)]有蘊含詞、等值詞6/29/2023465.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、消蘊含詞和等值詞

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

6/29/2023475.2.1子句集(4)“?”作用原子謂詞沒有量詞(、)合取范式元素之間變元不同集合形式?jīng)]有蘊含詞、等值詞6/29/2023485.2.1子句集(5)x{?yP(x，y)?y[?Q(x,y)R(x,y)]}

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

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

(x)雙重否定律摩根定律量詞轉換定律=>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)]}6/29/2023495.2.1子句集(6)“?”作用原子謂詞沒有量詞(、)合取范式元素之間變元不同集合形式?jīng)]有蘊含詞、等值詞6/29/2023505.2.1子句集(7)=>x{y?P(x，y)z[Q(x,z)?R(x,z)]}3、適當改名，使變量標準化即：對于不同的約束，對應于不同的變量x{y?P(x，y)y[Q(x,y)?R(x,y)]}問題:不同轄域的相同變元對應的約束相同嗎?6/29/2023515.2.1子句集(8)4、

消去存在量詞(Skolem化）,同時進行變元替換

原則：

①若該存在量詞不在任何全稱量詞的轄域內，則用一個常量符號代替該存在量詞轄域內的相應約束變元，

這個常量叫Skolem常量；②若該存在量詞在全稱量詞的轄域內，則用這些全稱量詞指導變元的一個函數(shù)代替該存在量詞轄域內的相應約束變元，這樣的函數(shù)稱為Skolem函數(shù)。理論依據(jù)：

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

存在指定規(guī)則6/29/2023525.2.1子句集(9)問題:為什么受全稱量詞約束的要用Skolem函數(shù)替換?而不能用常量替換？xyM（y，x）：對任意一個人x，都存在一個y，y是x的媽媽。若去掉存在量詞用常量a代替y，則變?yōu)椋簒M（a，x）：a是所有人的媽媽。實際上，引入Skolem函數(shù)，是由于存在量詞在全稱量詞的轄域之內，其約束變元的取值完全依賴于全稱變量的取值。而Skolem函數(shù)反映了這種依賴關系。6/29/2023535.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、消去所有全稱量詞。理論依據(jù)：

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

全稱指定規(guī)則6/29/2023545.2.1子句集(11)子句集的特征“?”作用原子謂詞沒有量詞(、)合取范式元素之間變元不同集合形式?jīng)]有蘊含詞、等值詞6/29/2023555.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))]

分配律6/29/2023565.2.1子句集(13)子句集的特征“?”作用原子謂詞沒有量詞(、)合取范式元素之間變元不同集合形式?jīng)]有蘊含詞、等值詞6/29/2023575.2.1子句集(14)=>[?P(x，f(x))Q(x,g(x))][?P(y，f(y))?R(y,g(y))]7、適當改名，使子句間無同名變元=>{?P(x，f(x))Q(x,g(x)),?P(y，f(y))?R(y,g(y))}8、消去合取詞，以子句為元素組成一個集合S=>

?P(x，f(x))[Q(x,g(x))?R(x,g(x))]6/29/2023585.2.1子句集-小結消去蘊含詞和等值詞使否定詞僅作用于原子公式使量詞間不含同名指導變元消去存在量詞消去全稱量詞化公式為合取范式子句間無同名變元組成一個集合“?”作用原子謂詞沒有量詞(、)合取范式元素之間變元不同集合形式?jīng)]有蘊含詞、等值詞蘊含等價式雙重否定律、摩根定律、量詞轉換律存在指定、依賴關系全稱指定分配律6/29/2023595.2.1子句集-練習（1）練習：用謂詞公式表示下述命題。已知前提：（1）自然數(shù)都是大于零的整數(shù)。（2）所有整數(shù)不是偶數(shù)就是奇數(shù)。（3）偶數(shù)除以2是整數(shù)。結論：所有自然數(shù)不是奇數(shù)就是除以2為整數(shù)的數(shù)。化F1F2F3

?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)))6/29/2023605.2.1子句集-練習（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)}6/29/2023615.2.1子句集-練習（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)}6/29/2023625.2.1子句集-練習（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))6/29/2023635.2.1子句集-練習應用歸結原理證明定理（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]6/29/2023645.2.1子句集(18)Skolem標準型在求子句集的過程中，消去存在量詞之后，把所有全稱量詞都依次移到式子的最左邊（或者把所有的量詞都依次移到式子最左邊，再消去存在量詞），再將右部的式子化為合取范式，這樣得到的式子就是原公式的Skolem標準型。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))}消去合取詞和全稱量詞，就得到了原公式的子句集6/29/2023655.2.1子句集(19)例5.8設消去存在量詞用a代替x用f(y,z)代替u用g(y,z,v)代替w得到G的Skolem標準型進而得G的子句集為：

一個謂詞公式的子句集也可以通過求前束范式（如果謂詞公式中一切量詞都位于該公式最左邊，不含否定詞，且量詞的轄域都延伸到公式末端），再求Skolem標準型而得到。6/29/2023665.2.1子句集(20)

引入Skolem函數(shù)，是由于存在量詞在全稱量詞的轄域內，其約束變元的取值完全依賴于全稱量詞的取值。Skolem函數(shù)反映了這種依賴關系。但Skolem標準型與原公式一般并不等價。

有公式：G＝xP(x)它的Skolem標準型是G’＝P(a)我們給出如下的解釋I：D＝{0,1},a/0,P(0)/F,P(1)/T在此解釋下，G＝T,G’＝F6/29/2023675.2.1子句集(21)定理1：謂詞公式G不可滿足當且僅當其子句集S不可滿足定義3：子句集S是不可滿足的，當且僅當其全部子句的合取式是不可滿足的。謂詞公式正確性證明謂詞公式否定式不可滿足性證明謂詞公式對應子句集的不可滿足性證明6/29/2023685.2.2命題邏輯中的歸結原理(1)歸結原理的提出歸結原理(principleofresolution)又稱消解原理,1965年魯濱遜（J.A.Robinson）提出，從理論上解決了定理證明問題。歸結原理提出的是一種證明子句集不可滿足性，從而實現(xiàn)定理證明的一種理論及方法。歸結原理的基本原理是采用反證法（反演推理方法）歸結算法是一節(jié)謂詞邏輯中的半可判定算法，對一階邏輯中任意恒真公式使用歸結原理，總可以在有限步內給以判定（證明其為永真）對不知該公式是否為恒真時，使用歸結原理得不到任何結論6/29/2023695.2.2命題邏輯中的歸結原理(2)定義4設L為一個文字，則L與?L為互補文字。

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

歸結式，C1、C2稱為其歸結式的親本子句，稱L1、L2為消解基。例5.9設，則C1、

C2的歸結式為：

6/29/2023705.2.2命題邏輯中的歸結原理(3)定理2歸結式是其親本子句的邏輯結果。證明：設C1=LC1’，C2=?LC2’其中C1’、C2’都是文字的析取式。

C1、C2的歸結式為C1’C2’

C1、C2的邏輯結果為：

C1=C1’L=?C1’→

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

C1∧

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

C2’=C1’C2’命題邏輯中的歸結原理：6/29/2023715.2.2命題邏輯中的歸結原理(4)例5.10用歸結原理驗證分離規(guī)則和拒取式

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

解

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

6/29/2023725.2.2命題邏輯中的歸結原理(5)類似的可以驗證其他推理規(guī)則。這說明，歸結原理可以代替其他所有的推理規(guī)則，而且推理步驟比較機械，為機器推理提供了方便。由歸結原理可知：L∧?L＝NIL另外我們知道：L∧?L＝F（假），也就是

NILF空子句就是恒假子句6/29/202373補充：定理1G為F1,F2,…，F(xiàn)n的邏輯結論，當且僅當（F1F2…Fn）=>G定理2G為F1,F2,…，F(xiàn)n的邏輯結論，當且僅當(F1F2…Fn)﹁G是不可滿足的。6/29/2023745.2.2命題邏輯中的歸結原理(6)利用歸結原理證明命題公式的思路先求出要證明的命題公式的否定式的子句集S；然后對子句集S（一次或者多次）使用歸結原理；若在某一步推出了空子句，即推出了矛盾，則說明子句集S是不可滿足的，從而原否定式也是不可滿足的，進而說明原公式是永真的。6/29/2023755.2.2命題邏輯中的歸結原理(7)推出空子句就說明子句集不可滿足，原因是：空子句就是F，推出空子句就是推出了F。歸結原理是正確的推理形式，由正確的推理形式推出了F，則說明前提不真，即歸結出空子句的兩個親本子句至少有一個為假。如果這兩個親本子句都是原子句集S中的子句，即說明原子句集S不可滿足。（因子句間為合取關系）如果這兩個親本子句不是或不全是S中的子句，那么它們必定是某次歸結的結果。同樣的道理向上回溯，一定會推出原子句集中至少有一個子句為假，從而說明S不可滿足。6/29/2023765.2.2命題邏輯中的歸結原理(8)推論設C1、C2是子句集S的兩個子句，C12是它們的歸結式，則（1）若用C12來代替C1、C2，得到新的子句集S1，則由S1不可滿足性可以推出原子句集S的不可滿足性。即（2）若用C12加入到S中，得到新的子句集S2，則S2與原S的同不可滿足。即S1的不可滿足性=>S不可滿足S2的不可滿足性<=>S不可滿足6/29/2023775.2.2命題邏輯中的歸結原理(9)例5.12設公理集：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（目標求反）

6/29/2023785.2.2命題邏輯中的歸結原理(10)子句集： (1)P (2)?P?QR (3)?SQ (4)?TQ (5)T (6)?R（目標求反）歸結： (7)?P?Q(2,6) (8)?Q (1,7)(9)?T(4,8)(10)NIL(5,9)?P?QR?R?P?QP?Q?TQ?TTNIL6/29/2023795.2.2命題邏輯中的歸結原理(11)例5.11證明子句集{P?Q,?P,Q}是不可滿足。證明：子句集： (1)P?Q (2)?P (3)Q歸結： (4)?Q由（1）和（2） (5)NIL由（4）和（5）得證6/29/2023805.2.3替換與合一(1)問題

在一階謂詞中應用消解原理，因為謂詞邏輯中的子句含有個體變元，所以可能無法直接找到互否文字的子句對例如：P(x)Q(z),?P(f(y))R(y)

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

對個體變元做適當替換例如：P(f(y))Q(z),?P(f(y))R(y)

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

表達式：項、原子公式、文字、子句的統(tǒng)稱?；磉_式：沒有變元的表達式。子表達式：出現(xiàn)在表達式E中的表達式稱為E的子表達式。定義7設θ={t1/x1,t2/x2,…,tn/xn}是一個替換，E是一個表達式，對E實施替換θ，即把E中出現(xiàn)的個體變元xj都用tj替換，記為Eθ,所得的結果稱為E在θ下的例（instance）。例如：若θ={a/x,f(b)/y,c/z},G=P(x,y,z)

Gθ=P(a,f(b),c)6/29/2023845.2.3替換與合一(4)定義8設θ＝{t1/x1,t2/x2,…,tm/xm}，λ＝{u1/y1,u2/y2,…,un/yn}是兩個替換，則將{t1λ/x1,t2λ/x2,…,tmλ/xm,u1/y1,u2/y2,…,un/yn}中符合下列條件的元素刪除

（1）tiλ

/xi當tiλ

＝

xi

（2）ui/yi當yi∈

{x1,…,xm}這樣得到的集合為θ與λ的復合或乘積，記為θ?λ。例：設θ={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}6/29/2023855.2.3替換與合一(5)定義9設S＝{F1,F2,…,Fn}

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

=F2θ=…=Fnθ，則稱θ為S的一個合一，稱S為可合一的。例：S={P(x,f(y),b),P(z,f(b),b)}替換θ={a/x,b/y,a/z}是S的一個合一,因為： 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的一個合一。一個公式的合一一般不唯一6/29/2023865.2.3替換與合一(6)定義10設σ是原子公式集S的一個合一，如果對S的任何一個合一θ都存在一個替換λ，使得

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

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

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

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

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

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

，k＝k+1，然后轉Step2；Step5：算法停止，S的最一般合一不存在。6/29/2023895.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。6/29/2023905.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)｝，由于變元y在項f(y)中出現(xiàn)，所以算法停止，S不存在最一般合一。

6/29/2023915.2.3替換與合一(11)定理3(合一定理)S是非空有限可合一的公式集，則合一算法總在Step2停止，且最后的σk即是S的最一般合一（MGU）。對任一非空有限可合一的公式集，一定存在最一般合一，而且用合一算法一定能找到最一般合一，即算法終止在第2步時最后的合一σk從合一算法可以看出，一個公式集S的最一般合一可能是不唯一的。如果差異集Dk=｛ak,bk｝，且ak和bk都是個體變元，則下面兩種選擇都是合適的：σk+1=σk·｛bk/ak｝或σk+1=σk·｛ak/bk｝6/29/2023925.2.4謂詞邏輯中的歸結原理(1)例：P(x)Q(y),?P(f(z))R(z) =>Q(y)R(z)定義12設C1，C2為無相同變元的子句；L1，L2為其中的兩個文字;L1和?L2有最一般合一σ；則C1，C2的二元歸結式（二元消解式）為：

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

6/29/2023935.2.4謂詞邏輯中的歸結原理(2)例5.18設C1=P(x)∨Q(x),C2=?P(a)∨R(y)，求C1,C2的歸結式。解取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的二元歸結式。6/29/2023945.2.4謂詞邏輯中的歸結原理(3)

例5.19設C1=P(x,y)∨Q(a),C2=?Q(x)∨R(y),求C1,C2的歸結式。解由于C1,C2中都含有變元x,y，所以需先對其中一個進行改名,方可歸結。2、如果在參加歸結的子句內部含有可合一的文字，則在進行歸結之前，也應對這些文字進行合一，從而使子句達到最簡。歸結過程需要注意兩點：1、兩個子句含有相同的變元，需要對其中一個進行改名6/29/2023955.2.4謂詞邏輯中的歸結原理(4)例如，設有兩個子句：C1=P(x)∨P(f(a))∨Q(x)C2=?P(y)∨R(b)可見,在C1中有可合一的文字P(x)與P(f(a))取替換θ={f(a)/x}現(xiàn)在再用C1θ與C2進行歸結，從而得到C1與C2的歸結式Q(f(a))∨R(b)則得C1θ=P(f(a))∨Q(f(a))6/29/2023965.2.4謂詞邏輯中的歸結原理(5)例5.20：C＝P(x)P(f(y))?Q(x),σ={f(y)/x}

Cσ＝P(f(y))?Q(f(y))是C的因子。定義13子句C中，兩個或兩個以上的文字有一個最一般合一σ，則稱Cσ為C的因子，若Cσ為單元子句，則Cσ稱為C的單因子。6/29/2023975.2.4謂詞邏輯中的歸結原理(6)定義14子句的C1，C2消解式，是下列二元消解式之一:

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

C1

C2

＝>（C1

σ－{L1

σ}）∪（

C2σ－{L2σ}）

其中C1、C2是兩個無相同變元的子句，L1，L2分別是C1，C2中的文字,σ為L1和?L2的最一般合一。6/29/2023995.2.4謂詞邏輯中的歸結原理(8)例5.21求證G是A1和A2的邏輯結果。A1：(x)(P(x)(Q(x)R(x)))

A2

：(x)(P(x)S(x))G：(x)(S(x)R(x))證：利用歸結反演法，先證明A1A2?G是不可滿足的。a.求子句集：

(1)?P(x)Q(x)(2)?P(y)R(y)(3)P(a)(4)S(a)(5)?S(z)?R(z)(?G)A2A1S6/29/20231005.2.4謂詞邏輯中的歸結原理(9)b.應用消解原理，得：(6)R(a)[(2),(3),σ1={a/y}](7)?R(a)[(4),(5),σ2={a/z}](8)Nil[(6),(7)]c.所以S是不可滿足的，從而G是A1和A2的邏輯結果。a.求子句集S

(1)?P(x)Q(x)(2)?P(y)R(y)(3)P(a)(4)S(a)(5)?S(z)?R(z)6/29/2023101求取謂詞邏輯的歸結式要注意謂詞的一致性：名稱不一致的謂詞P與?Q不能歸結常量的一致性：含有不同常量的謂詞不能歸結，如P(a,…)和?P(b,…)不能歸結，但同樣謂詞，常量與變元不同時，P(a,…)和?P(x,…)可以替換合一轉化成相同形式再歸結變元與函數(shù)：P(x,x…)和?P(f(x),f(x)…)不能歸結,因為不存在替換{f(x)/x}，但P(x,x…)和?P(f(y),f(y)…)可歸結,因為存在替換{f(y)/x}，不能同時消去兩個互補對：P(x)Q(x)和?P(x)?Q(x)不能直接得到□，因為真值證明(P(x)Q(x))(?P(x)?Q(x))不是矛盾式，推不出空子句。但P(x)P(y)和?P(u)?P(v)可以合一替換歸結得到□，6/29/20231025.2.4謂詞邏輯中的歸結原理(10)例5.22設已知：（1）能閱讀者是識字的；（2）海豚不識字；（3）有些海豚是很聰明的。試證明：有些聰明者并不能閱讀。證首先定義如下謂詞：R(x):x能閱讀。L(x):x能識字。I(x):x是聰明的。D(x):x是海豚。將上述各語句翻譯成謂詞公式：(1)(x)(R(x)L(x))(2)(x)(D(x)?L(x))已知條件(3)(x)(D(x)I(x))(4)(x)(I(x)?R(x))需證結論6/29/20231035.2.4謂詞邏輯中的歸結原理(11)用歸結反演法來證明，求題設與結論否定的子句集，得：

(1)?

R(x)L(x)(2)?

D(y)?L(y)（改名）(3)D(a)(4)I(a)(5)?I(z)R(z)歸結得：(6)R(a)[(5),(4),{a/z}](7)L(a)[(6),(1),{a/x}](8)?D(a)[(7),(2),{a/y}](9)Nil[(8),(3)]?I(z)R(z)R(a)L(a)?D(a)NilI(a)?R(x)L(x)?D(y)L(y)D(a)6/29/20231045.2.4謂詞邏輯中的歸結原理(12)定理5如果子句集S是不可滿足的，那么必存在一個由S推出空子句的消解序列。證明從略6/29/20231055.2.4謂詞邏輯中的歸結原理(13)練習設已知：（1）自然數(shù)都是大于零的整數(shù)；（2）所有整數(shù)不是偶數(shù)就是奇數(shù)；（3）偶數(shù)除以2是整數(shù)。試證明：所有自然數(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。將上述各語句翻譯成謂詞公式：

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)))6/29/20231065.2.4謂詞邏輯中的歸結原理(14)利用歸結反演法，先證明F1F2F3?G是不可滿足的。F1F2F3?G的子句集為（1）?N(x)GZ(x)（2）?N(y)I(y)（4）?E(u)I(s(u))（3）?I(z)E(z)O(z)（5）N(a)（6）?O(a)（7）?I(s(a))6/29/2023107應用歸結原理進行定理證明的方法思路寫出定理的謂詞公式用反演法表達謂詞公式化為Skolem標準型求取子句集S對S中可歸結的子句做歸結歸結式仍放在S中，反復執(zhí)行歸結過程得到空子句得證。6/29/20231085.3應用歸結原理求取問題答案(1)例5.23已知：（1）如果x和y是同班同學，則x的老師也是y的老師。（2）王先生是小李的老師。（3）小李和小張是同班同學。問：小張的老師是誰？解首先定義如下謂詞：

T(x,y)表示x是y的老師

C(x,y)表示x與y是同班同學。

已知條件可以表示成如下謂詞公式：F1：xyz(C(x,y)T(z,x)T(z,y))F2:T(Wang,Li)F3:C(Li,Zhang)

6/29/20231095.3應用歸結原理求取問題答案(2)

為了得到答案，首先要證明小張的老師是存在的。即證明：G：xT(x,Zhang)

(1)?C(x,y)?T(z,x)T(z,y)