二叉树的 Herbrand 宇宙、Herbrand 基础和 Herbrand 模型（序言）

什么是二叉树的 Herbrand 宇宙、Herbrand Base 和 Herbrand Model：

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

Herbrand 宇宙是给定签名的基本术语。许多序言 系统有一个谓词ground/1，你可以用它来检查一个术语是否是 实际上是接地的。 ground/1 的定义是它不包含变量：

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

Herbrand 基础是给定签名的基本素数公式。 A 素数公式是谓词或等式。您还可以使用地面/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 基地本身始终是一个典范。喇叭条款连同 克拉克方程理论还有一个独特的最小赫布兰德模型。这是 Herbrand 程序算子的固定点。程序的某些属性 运算符允许声明可以在阶段 omega 达到固定点。

但使用 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 ，即 上述递推关系的最小不动点。好像 没有说什么。