Herbrand宇宙，Herbrand基地和二叉树的Herbrand模型（序言）(Herbrand

什么是Herbrand宇宙，Herbrand基地和二叉树的Herbrand型号：

binary_tree(empty). 
binary_tree(tree(Left,Element,Right)) :- 
     binary_tree(Left), 
     binary_tree(Right).

该Herbrand宇宙是一个定签名的地面条件。许多Prolog的系统有一个谓词地面/ 1，你可以用它来检查某个项目是否实际上是地面。地面/ 1的定义是，它不包含变量：

?- ground(empty).
Yes
?- ground(tree(X,Y,Z)).
No

该Herbrand基是一个给定签名的地面黄金公式。一个最好的配方是谓词或相等。您也可以使用地面/ 1，检查的黄金公式是地面：

?- ground(a = X).
No
?- ground(a = b).
Yes
?- ground(binary_tree(X)).
No
?- ground(binary_tree(tree(empty,n,empty))).
Yes

一个Herbrand模型是一个模型，其中的宇宙是一个Herbrand宇宙。看作是一个图中的Herbrand模型是Herbrand基的子集。一个理论可能没有，有一个或多个Herbrand模型。

Horn子句总是有一个Herbrand模型，特别是全Herbrand模型，该模型是Herbrand基地本身，始终是一个典范。与克拉克等式理论Horn子句在一起也有一个独特的最小Herbrand模型。这是Herbrand程序操作的不动点。该程序操作的某些属性允许地指出，不动点可以在阶段欧米加到达。

但随着Herbrand模型时显得笨拙，因为它们没有排序。许多分类签名和相应的地面模型更加得心应手。为简单起见，并避免在目前情况下很多分类逻辑，我们可以假设你的程序读取，即树中的元素是皮亚诺的数字：

binary_tree(empty). 
binary_tree(tree(Left,Element,Right)) :- 
    binary_tree(Left),
    tree_element(Element), 
    binary_tree(Right).
tree_element(n).
tree_element(s(X)) :-
    tree_element(X).

那么你的二叉树的定义会导致以下递推关系：

T_0 = {}
T_n+1 = {binary_tree(empty)} u {binary_tree(tree(s,e,t)) | 
       binary_tree(s) in T_n, 
       tree_element(e) in T_n, 
       binary_tree(t) in T_n } u 
        {tree_element(n)} u {tree_element(s(e)) |
       tree_element(e) in T_n} u T_n

然后，将独特的最小Herbrand模型将是T = union_n T_n它是上述递推关系的至少固定点。看起来像什么也没有说。

再见