人工智能原理教案02章 歸結(jié)推理方法2.6 Herbrand定理.doc

2.6 Herbrand定理Herbrand定理是歸結(jié)原理的理論基礎(chǔ)，歸結(jié)原理的正確性是通過Herbrand定理來證明的。同時歸結(jié)原理是Herbrand定理的具體實現(xiàn)，利用Herbrand定理對公式的證明是通過歸結(jié)法來進行的。本節(jié)簡單地描述了Herbrand定理的基本思想和相關(guān)預(yù)備知識，最后給出Herbrand定理的一般形式。 公式G永真：對于G的所有解釋，G都為真。公式G永假（矛盾）： 沒有一個解釋使G為真。2.6.1 Herbrand 定理概述問題：一階邏輯公式的永真性（永假性）的判定是否能在有限步內(nèi)完成？1936年圖靈(Turing)和邱吉(Church)互相獨立地證明了：沒有一般的方法使得在有限步內(nèi)判定一階邏輯的公式是否是永真（或永假）。但是如果公式本身是永真（或永假）的，那么就能在有限步內(nèi)判定它是永真（或永假）。對于非永真（或永假）的公式就不一定能在有限步內(nèi)得到結(jié)論。判定的過程將可能是不停止的。2.6.1.1 Herbrand 定理思想要證明一個公式是永假的，采用反證法的思想（歸結(jié)原理），就是要尋找一個已給的公式是真的解釋。然而，如果所給定的公式的確是永假的，就沒有這樣的解釋存在，并且算法在有限步內(nèi)停止。因為量詞是任意的，所討論的個體變量域D是任意的，所以解釋的個數(shù)是無限、不可數(shù)的，要找到所有的解釋是不可能的。Herbrand 定理的基本思想是簡化討論域，建立一個比較簡單、特殊的域，使得只要在這個論域上（此域稱為H域），原謂詞公式仍是不可滿足的，即保證不可滿足的性質(zhì)不變。H域和D域關(guān)系的如下圖表示：圖21 H域與D域關(guān)系示意圖t2-1_swf.htm2.6.1.2 H域H域的定義：設(shè)S為給定公式G的子句集，定義在論域D上，H0為S中的常量集。如果S中沒有常量，H0由任意單個常量構(gòu)成，如a，Hi+1= Hifm(t1, t2, tn), i=0, 1, 其中，fm為S中出現(xiàn)的所有函數(shù)符號的集合，t1, t2, tn為Hi-1的元素，i1，2, 則規(guī)定H稱為G的H域（或說是相應(yīng)的子句集S的H域）。Hi稱為S的i水平常量集。不難看出，H域是直接依賴于G的，而且最多只有可數(shù)個元素。 例題2-4設(shè)子句集S = P(x), Q(y,f(z,b),R(a)，求H域解：H0 a, b為子句集中出現(xiàn)的常量H1 a, b, f(a,b), f(a,a), f(b,a), f(b,b)H2 a, b, f(a,b), f(a,a), f(b,a), f(b,b)， f(a,f(a,b), f(a,f(a,a), f(a, f(b,a), f(a, f(b,b), f(b,f(a,b), f(b,f(a,a), f(b, f(b,a), f(b, f(b,b), f(f(a,b),f(a,b), f(f(a,b),f(a,a), f(f(a,b), f(b,a), f(f(a,b), f(b,b), f(f(a,a),f(a,b), f(f(a,a),f(a,a), f(f(a,a), f(b,a), f(f(a,a), f(b,b), f(f(b,a),f(a,b), f(f(b,a),f(a,a), f(f(b,a), f(b,a), f(f(b,a), f(b,b), f(f(b,b),f(a,b), f(f(b,b),f(a,a), f(f(b,b), f(b,a), f(f(b,b), f(b,b)H = H1H2H3解畢注意：一個函數(shù)中含有多個變量時，每個變量都要做到全部的組合。原子集A：為研究子句集S中的不可滿足性，需要討論H域上S中各謂詞的真值。這里原子集A為公式中出現(xiàn)的謂詞套上H域的元素組成的集合。A = 所有形如 P(t1, t2, tn)的元素。這里，P(x1, xn)為出現(xiàn)于S中的任一謂詞符號，而t1, t2, tn為S的H域中的任意元素。即把H域中的東西填到S的謂詞里去。上例題的原子集為：A = P(a), Q(a,a), R(a), P(b), Q(b,a), Q(b,b), Q(b,a), R(b), P(f(a,b), Q(f(a,b), f(a,b), R(f(a,b), P(f(a,a), P(f(b,a), P(f(b,b),) 一旦原子集內(nèi)真值確定好（規(guī)定好），則S在H上的真值可確定。不可數(shù)問題轉(zhuǎn)化成為了可數(shù)問題。S中的謂詞是有限的，H是可數(shù)的，因此，A也是可數(shù)的。論域D上公式G或子句集S的H域的建立，僅依賴于S中出現(xiàn)的幾個函數(shù)符號，以及S中出現(xiàn)的D的幾個常量符號，或D中的一個常量符號，這些都是可數(shù)的H域比一般論域D簡單的原因。2.6.1.3 H解釋解釋I：謂詞公式G在論域D上任何一組真值的指定稱為一個解釋。H解釋：子句集S在H域上的解釋稱為H解釋。I是H域下的一個指派。簡單地說，原子集A中的各元素真假組合都是H的解釋（或真或假只取一個）?；蛘哒f凡對A中各元素真假值的一個具體設(shè)定，都是S的一個H解釋。由子句集S建立H域、原子集A，希望定義于一般論域D上使S為真的任一解釋I，可由依于S的H域上的某個解釋I*來實現(xiàn)。這樣，便使任意論域D上S為真的問題，化成了僅有可數(shù)個元素的H域上S為真的問題了。從而子句集S在D上不可滿足問題化成了H上的不可滿足的問題。幾個術(shù)語的定義：沒有變量出現(xiàn)的原子、文字、子句和子句集，分別稱為基原子、基文字、基子句和基子句集?；鹤泳浼疭中某子句C中所有變元符號均以S的H域中的元素代入時，所得的基子句C稱為C的一個基例。若一個解釋I*使得某個基子句為假，則此解釋I*為假。例：SP(x)Q(x), R(f(y)，求其一個H解釋I*解：S的H域為：a, f(a), f(f(a), S的原子集為：P(a), Q(a), R(a), P(f(a), Q(f(a), R(f(a), 凡對A中各元素真假值的一個具體設(shè)定都為S的一個H解釋。如：I1*P(a), Q(a), R(a), P(f(a), Q(f(a), R(f(a), I2*P(a), Q(a), R(a), P(f(a), Q(f(a), R(f(a), I3*P(a), Q(a), R(a), P(f(a), Q(f(a), R(f(a), I1*，I2*，I3*中出現(xiàn)的P(a)表示P(a)的取值為T，出現(xiàn)的P(a)表示P(a)的取值為F。顯然在H域上，這樣的定義I*下，S的真值就確定了。如：S| I1*T，S| I2*F，S| I3*F這是因為子句集SP(x)Q(x), R(f(y)的邏輯含義為：(x)(y)(P(x)Q(x)R(f(y)，論域H為a, f(a), f(f(a), 。關(guān)鍵：對于公式G的所有的解釋，如果公式取值全為假，才可以判定G是不可滿足的。因為所有解釋代表了所有的情況，如果這些解釋可以被窮舉，我們就可以在有限的步數(shù)內(nèi)判斷公式G的不可滿足性，本小節(jié)開始所提的問題便可解決 。我們所關(guān)心的是，對論域D上的任一個解釋，若有S|I = T，如何求得一個相應(yīng)的H解釋，使得S|I* = T成立?？梢宰C明，有如下三個定理：定理：定理1：設(shè)I是S的論域D上的解釋，存在對應(yīng)于I的H解釋I*，使得若有S|I = T，必有 S|I* = T。定理2：子句集S是不可滿足的，當且僅當S的一切H解釋都為假。 定理3：子句集S是不可滿足的，當且僅當對每一個解釋I下，至少有S的某個子句的某個基例為假。以上三個定理保證了歸結(jié)法的正確性。因為它們把S在一般論域D上的不可滿足問題化成了可數(shù)集H上的不可滿足問題。今后的討論只需在S的H域上進行了，不必再涉及一般論域D。對于定理3來說，其結(jié)果經(jīng)常被引用。因為S的邏輯含義是所包含的子句的合取，而且變量受全稱量詞的作用。那么在某個解釋I（均指H解釋）下為假，只需某個子句的某個基例為假，而S是不可滿足的，要求在任一解釋下均為假，從而定理3成立。 一般來說，D域是無窮不可列的，因此，子句集也是無窮不可列的。但子句集S確定后其H域是無窮可列的。不過在H上證明S的不可滿足性仍然是不可能的。解決問題的方法：語義樹。2.6.2 語義樹與Herbrand定理對S的不可滿足性，從幾何上進行一些討論是有益的?？梢詫⒆泳浼疭的所有可能解釋展示在一棵樹上，進而觀察每個分枝對應(yīng)的S的邏輯真值是真是假。語義樹的構(gòu)成方法如下原子集A中所有元素逐層添加到一棵二叉樹，并將元素的是與非分別標記在兩側(cè)的分枝上。下面是一個語義樹的例子：例：對子句集SP(x)Q(x)，P(f(y)，Q(f(y)，畫出相應(yīng)的語義樹。解：子句集S的H域為：Ha，f(a)，f(f(a)，原子集為AP(a)，Q(a)，P(f(a)，Q(f(a)，從A出發(fā)便可畫出S的語義樹，如下圖所示：圖2-2 無限語義樹t2-2_swf.htm一般情況H是無限可數(shù)集，因此，S的語義樹是無限樹。 語義樹的意義語義樹可以理解為H域的圖形解釋。通過子句集S H域 原子集A 語義樹?？梢钥闯?，我們討論的對象從無限、不可數(shù)論域D轉(zhuǎn)換成為可數(shù)的、有序的語義樹。定義：完全語義樹：S的語義樹是完全的，如果對該語義樹的所有葉結(jié)點N來說，I(N)包含了S的原子集AA1，A2，中的所有元素Ai或Ai，i=1 n 建立語義樹的目的是把S中的每個解釋都攤開。通過對S的完全語義樹的觀察，如上例的語義樹圖，這棵樹的每個直到葉結(jié)點的分枝都對應(yīng)于S的一個解釋。特別對有限樹來說，若N是葉結(jié)點，那么I(N)便是S的一個解釋。討論S的不可滿足性，就可通過對語義樹的每個分枝計算S的每一個解釋的真值而實現(xiàn)。 有時并非需要無限地延伸某個分枝方能確定在相應(yīng)的解釋下S取假值。如果某個分枝延伸到結(jié)點N時，I(N)已使S的某一子句的某一基例為假，就無需再對N作延伸了。定義失敗結(jié)點：當（由上）延伸到點N時，I(N)已表明了S的某子句的某個基例為假。但N以前尚不能判斷這事實。就稱N為失敗結(jié)點。 封閉語義樹：如果S的完全語義樹的每個分枝上都有一個失敗結(jié)點，就稱它是一棵封閉語義樹。圖2-2所示的完全語義樹便具有每個分枝上都有失敗結(jié)點這樣的性質(zhì)，從而是一棵封閉的語義樹。如果從圖2-2剪去所有失敗結(jié)點以下的分枝，便得相應(yīng)的封閉語義樹，見圖2-3：圖2-3 封閉語義樹t2-3_swf.htm如I(N22)P(a)，Q(a)，這個S的部分解釋已使S中的子句P(x)Q(x)的基例P(a)Q(a)為假了，而N11，N0不具有這個性質(zhì)。若將I(N22)進一步擴充，仍然會使S為假，擴充的部分對使S為假已經(jīng)不起作用了。從圖上看無需對N22再作延伸了。Herbrand定理：定理1：子句集S是不可滿足的，當且僅當對應(yīng)于S的完全語義數(shù)是棵有限封閉樹。 定理2：子句集S是不可滿足的，當且僅當存在不可滿足的S的有限基例集。 定理的意義在于將一階邏輯證明問題轉(zhuǎn)化成了有限的命題邏輯問題。由此定理保證，可以放心的用機器來實現(xiàn)自動推理了。（歸結(jié)原理）注意：Herbrand定理給出了一階邏輯的半可判定算法，即僅當被證明定理是成立時，使用該算法可以在有限步得證。而當被證定理并不成立時，使用該算法得不出任何結(jié)論。使用Herbrand定理，來證明定理或S是不可滿足的，或是尋找有限的封閉樹或是尋找有限的不可滿足的基例集。一個具體實現(xiàn)證明的方法