Herbrand universe, Herbrand Base and Herbrand Mode

问题:

What is the Herbrand universe, Herbrand Base and Herbrand Model of binary tree:

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

回答1:

The Herbrand universe are the ground terms of a given signature. Many Prolog systems have a predicate ground/1 which you can use to check whether a term is actually ground. The definition of ground/1 is that it doesn't contain variables:

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

The Herbrand base are the ground prime formulas of a given signature. A prime formula is a predicate or an equality. You can also use ground/1 to check whether a prime formula is ground:

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

A Herbrand model is a model where the universe is a Herbrand universe. Viewed as a diagram a Herbrand model is a subset of a Herbrand base. A theory might have none, one or many Herbrand models.

Horn Clauses always have a Herbrand model, in particular the full Herbrand model which is the Herbrand base itself, is always a model. Horn Clauses together with the Clark Equational Theory also have a unique minimal Herbrand model. Which is the fixpoint of the Herbrand program operator. Certain properties of the program operator allow to state that the fixpoint can be reached at stage omega.

But working with Herbrand models is clumsy, since they are not sorted. Many sorted signatures and corresponding ground models are more handy. For simplicity and to avoid many sorted logic in the present case we could assume that your program reads, i.e. that the tree elements are peano numbers:

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).

Then your binary tree definition would lead to the following recurrence relation:

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

The unique minimal Herbrand model would then be T = union_n T_n which is the least fixpoint of the above recurrence relation. Looks like nothing has been said.

Bye