Herbrand宇宙和最少herbrand模型

Question

我讀了Herbrand universe, Herbrand Base and Herbrand Model of binary tree (prolog)問及問題的答案，但我有一個稍微不同的問題更像是一個確認，並希望我的困惑將澄清。

設P爲一個程序，我們有以下的事實和規則：

q(a, g(b)). 
q(b, g(b)). 
q(X, g(X)) :- q(X, g(g(g(X)))). 

從上面的計劃，Herbrand宇宙

Up = {a, b, g(a), g(b), q(a, g(a)), q(a, g(b)), q(b, g(a)), q(b, g(b)), g(g(a)), g(g(b))...e.t.c} 

Herbrand基地：

Bp = {q(s, t) | s, t E Up} 

• 現在來我的問題（原諒我爲我的無知），我包括q（a，g（a））作爲Herbrand宇宙中的一個元素，但是從它的事實表明q（a，g（b））。這是否意味着q（a，g（a））不應該在那裏？
• 此外，由於Herbrand模型是Herbrand基礎的子集，我如何通過歸納確定最小Herbrand模型？

注：我已經做了大量的研究，有些部分對我來說很清楚，但我仍然有這個疑問，這就是爲什麼我想尋求社區意見。謝謝。

Answer 1

從事實q(a,g(b))你不能斷定q(a,g(a))是否在模型中。你將不得不首先生成模型。

要確定模型，請從事實{q(a,g(b)), q(b,g(b))}開始，現在嘗試應用您的規則來擴展它。但是，在您的情況下，無法將規則q(X,g(X)) :- q(X,g(g(g(X)))).的右側與上述事實相匹配。因此，你完成了。

現在想象規則

q(a,g(Y)) :- q(b,Y). 

這條規則可以用來擴大我們的集合。事實上，實例

q(a,g(g(b))) :- q(b,g(b)). 

用於：如果q(b,g(b))存在，得出結論q(a,g(g(b)))。請注意，我們在這裏使用從右到左的規則。所以我們獲得

{q(a,g(b)), q(b,g(b)), q(a,g(g(b)))} 

從而達到一個固定點。

現在採取的另一個例子中，你所建議的規則

q(X, g(g(g(X)))) :- q(X, g(X)). 

允許（我將不再顯示實例化的規則）在一個步驟中產生：

{q(a,g(b)), q(b,g(b)), q(a,g(g(g(b)))), q(b, g(g(g(b))))} 

但是這不是結束，因爲再一次，這個規則可以用來產生更多！事實上，你現在有一個無限的模型！

 
{g(a,gn+1(b)), g(b, gn+1(b))} 

---

當你試圖理解Prolog遞歸規則這從右到左的閱讀往往是非常有幫助的。自上而下的閱讀（從左到右）往往是相當困難的，特別是，因爲你必須考慮到回溯和一般的統一。

Answer 2

關於你的問題：「此外，由於該Herbrand模型是Herbrand基的子集，我怎麼通過感應確定至少Herbrand模型」

如果你有喇叭條款一組P，定程序，那麼你可以定義 程序操作：

T_P(M) := { H S | S is ground substitution, (H :- B) in P and B S in M } 

最少的型號是：

inf(P) := intersect { M | M |= P } 

請注意，並非確定程序的所有模型都是 程序運算符的固定點。例如，完整的herbrand模型始終是 程序P的一個模型，該模型顯示明確的程序總是一致的，但它不一定是固定點。

另一方面，程序操作員的每個固定點是確定程序的模型。也就是說，如果你有T_P（M）= M，那麼可以斷定 M | = P.這樣經過一些進一步的數學推理（*）可以發現 最少的不動點也是最模型：

lfp(T_P) = inf(P) 

但是我們需要進一步考慮，以便我們可以說我們可以通過一種計算來確定最小模型 。即一個很容易注意到， 程序操作是連續的，即保留鏈的無限工會，因爲 喇叭條款沒有FORALL在自己的身體量詞：

union_i T_P(M_i) = T_P(union_i M_i) 

所以這之後，再次一些進一步的數學推理（*）發現我們可以通過迭代計算最少的定點，女巫可以用於簡單的 歸納。最小模型的每一個元素都有有限 深度的簡單推導：

union_i T_P^i({}) = lpf(T_P) 

再見

（*） 最有可能你會發現在這本書中所需要的精確的數學推理 進一步的暗示，但遺憾的是我不記得哪些部分 是相關的：
基礎邏輯編程，約翰·懷利勞埃德，1984年
http://www.amazon.de/Foundations-Programming-Computation-Artificial-Intelligence/dp/3642968287