Herbrand宇宙、Herbrand基和Herbrand二叉树模型(prolog)

Question

什么是Herbrand宇宙，Herbrand基础和二叉树的Herbrand模型：

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

Answer 1

赫布兰德宇宙是给定签名的基本术语。许多Prolog系统都有一个谓词ground/1，您可以用它来检查一个术语是否真的是ground。ground/1的定义是它不包含变量：

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

Herbrand基是给定签名的基本素数公式。素数公式是谓词或等式。您还可以使用ground/1检查质数公式是否为ground：

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

赫布兰德模型是一种模型，其中宇宙就是赫布兰德宇宙。从图表的角度来看，Herbrand模型是Herbrand基础的子集。一个理论可能没有、可能有一个或多个赫布兰德模型。

Horn子句总是有一个Herbrand模型，特别是作为Herbrand基础本身的完整Herbrand模型，它始终是一个模型。Horn子句和Clark方程理论也有一个独特的最小Herbrand模型。这是Herbrand程序运算符的固定点。程序运算符的某些属性允许声明可以在阶段omega到达固定点。

但使用Herbrand模型是很笨拙的，因为它们没有排序。许多排序的签名和相应的地面模型更方便。为了简单起见，为了避免当前情况下的许多排序逻辑，我们可以假设您的程序是读取的，即树元素是peano数：

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

因此，唯一的最小赫布兰德模型将是T= union_n T_n，这是上述递归关系的最小固定点。看起来什么都没说。