9.4.1 反向鏈接算法

圖9.6顯示了一個(gè)簡單的反向鏈接算法，F(xiàn)OL-BC-ASK。它用只包含單個(gè)元素（即原始查詢）的目標(biāo)列表來調(diào)用，并返回滿足查詢的所有置換的集合。目標(biāo)列表可以認(rèn)為是一個(gè)等待處理的“棧”；如果所有的棧內(nèi)目標(biāo)都可以得到滿足，則當(dāng)前的證明分支是成功的。算法選取列表中的第一個(gè)目標(biāo)，在知識(shí)庫中尋找正文字（或稱為頭）能與該目標(biāo)合一的每個(gè)子句。每個(gè)這樣的子句創(chuàng)建一個(gè)新的遞歸調(diào)用，在該遞歸過程中，子句的前提（或稱為體）都被加入到目標(biāo)棧內(nèi)。記住事實(shí)就是只有頭沒有體的子句，因此當(dāng)目標(biāo)和某個(gè)已知事實(shí)合一時(shí)，不會(huì)有新的子目標(biāo)添加到棧里，目標(biāo)也就得到了解決。圖 9.7 是從語句（9.3）到（9.10）得到Criminal(West)的證明樹。

該算法采用置換的合成。COMPOSE(θ1, θ2)是個(gè)置換，其效果與依次應(yīng)用每個(gè)置換的效果完全相同。也就是，

SUBST(COMPOSE(θ1, θ2), p) = SUBST(θ2, SUBST(θ1, p))

在該算法中，存儲(chǔ)在θ 中的當(dāng)前變量綁定和用目標(biāo)與子句頭合一得到的綁定進(jìn)行合成，給出用于遞歸調(diào)用的當(dāng)前綁定的新集合。

圖9.6 一個(gè)簡單的反向鏈接算法

圖9.7 為了證明West是個(gè)罪犯而由反向鏈接構(gòu)造的證明樹。閱讀這棵樹的方法是深度優(yōu)先，從左到右。為了證明Criminal(West)，我們必須證明下面的4個(gè)合取子句。其中一些在知識(shí)庫中，另一些則需要進(jìn)一步的反向鏈接。每個(gè)成功合一的綁定顯示在相應(yīng)的子目標(biāo)旁邊。注意，一旦合取式中的某個(gè)子目標(biāo)得以成功實(shí)現(xiàn)，它的置換就可以用于后續(xù)子目標(biāo)。因此，當(dāng)FOL-BC-ASK到達(dá)最后一個(gè)合取子句時(shí)，即原來Hostile(z)時(shí)，z已經(jīng)被限制為Nono

反向鏈接，如同我們前面所寫，顯然是深度優(yōu)先搜索算法。這意味它的空間需求與證明的規(guī)模成線性關(guān)系（目前，忽略存儲(chǔ)答案所需的空間）。它還意味著反向鏈接（不像前向鏈接）要忍受重復(fù)狀態(tài)和不完備性問題的困擾。我們將討論這些問題和一些潛在的解決方案，但是我們首先來看看反向鏈接怎樣應(yīng)用于邏輯程序設(shè)計(jì)系統(tǒng)。