The Herbrand universe is the main term for this signature. Many Prolog systems have a ground / 1 predicate that you can use to check whether a term is actually based. The definition of the base / 1 is that it does not contain variables:
?- ground(empty). Yes ?- ground(tree(X,Y,Z)). No
Herbrand base - these are the basic simple formulas of this signature. a simple formula is a predicate or equality. You can also use ground / 1 to check if the basic formula is stated:
?- ground(a = X). No ?- ground(a = b). Yes ?- ground(binary_tree(X)). No ?- ground(binary_tree(tree(empty,n,empty))). Yes
The Herbrand Model is a model in which the universe is a Herbrand universe. Viewed as a diagram, the Herbrand model is a subset of the Herbrand base. A theory may not have one, not one, or several Herbrand models.
Horn Clauses always has a Herbrand model, in particular the complete Herbrand model which is the basis of Herbrand, is always a model. Horn clauses along with Clark's Equitable Theory also have a unique minimal Herbrand model. Which is the fixed point operator of the Herbrand program. The operator defines certain properties of the program that a fixed point can be reached at the omega stage.
But working with the Herbrand model is awkward, as they are not sorted. Many sorted signatures and corresponding ground models are more convenient. For simplicity and to avoid multidimensional logic, in this 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 definition of the binary tree will result in the following repetition ratio:
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 only minimal Herbrand model will then be T = union_n T_n, which is the smallest fixed point of the aforementioned recurrence relation. Looks like nothing was said.
Bye