prolog - Herbrand Universe，Herbrand Base和Herbrand二叉树模型(序言)

什么是Herbrand宇宙，Herbrand Base和Herbrand二叉树模型:

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基数是给定签名的基本基本公式。一种
素数公式是谓词或等式。您也可以使用地/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 Clauses始终具有Herbrand模型，尤其是完整的Herbrand模型
这是Herbrand基地本身，始终是典范。牛角条款与
克拉克方程理论也有一个独特的最小Herbrand模型。哪一个
Herbrand计划运营商的定位点。程序的某些属性
运算符(operator)允许声明在Ω阶段可以到达固定点。

但是使用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

唯一的最小Herbrand模型将为T = union_n T_n
上述重复关系的最小定点。好像
什么也没说。

再见

关于prolog - Herbrand Universe，Herbrand Base和Herbrand二叉树模型(序言)，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/11509350/