Herbrand model and the smallest herbrand model

Question

I read the question asked in the Universe Herbrand, Herbrand Base and Herbrand Model of a binary tree (prologue) and answers, but I have a slightly different question. as confirmation, and we hope that my confusion will be clarified.

Let P be such a program that we have the following facts and a rule:

q(a, g(b)). q(b, g(b)). q(X, g(X)) :- q(X, g(g(g(X)))). 

From the above Herbrand Universe program

 Up = {a, b, g(a), g(b), q(a, g(a)), q(a, g(b)), q(b, g(a)), q(b, g(b)), g(g(a)), g(g(b))...etc} 

Foundation of Herbrand:

 Bp = {q(s, t) | s, t E Up} 

• Now come to my question (sorry for my ignorance), I included q (a, g (a)) as an element in my Herbrand universe, but from what it indicates q (a, g (b)), Does Is it that q (a, g (a)) is not supposed to be there?
• Also, since Herbrand models are a subset of the Herbrand base, how can I determine the smallest Herbrand model by induction?

Note. I have done a lot of research on this, and some parts are clear to me, but still I have this doubt in me, so I want to find a community opinion. Thanks.

Answer 1

From the fact q(a,g(b)) you cannot infer whether q(a,g(a)) is in the model. First you need to generate a model.

To determine the model, start with the facts {q(a,g(b)), q(b,g(b))} and now try to apply your own rules to expand it. In your case, however, there is no way to map the right side of the rule q(X,g(X)) :- q(X,g(g(g(X)))). with the facts above. So you are done.

Now imagine the rule

 q(a,g(Y)) :- q(b,Y). 

This rule can be used to expand our set. In fact, an instance

 q(a,g(g(b))) :- q(b,g(b)). 

: If q(b,g(b)) present, enclose q(a,g(g(b))) . Please note that we use the rule from right to left here. So, we get

 {q(a,g(b)), q(b,g(b)), q(a,g(g(b)))} 

thereby reaching a fixed point.

Now take as another example you proposed a rule

 q(X, g(g(g(X)))) :- q(X, g(X)). 

Which allows (I will no longer show the created rule) for generation in one step:

 {q(a,g(b)), q(b,g(b)), q(a,g(g(g(b)))), q(b, g(g(g(b))))} 

But this is not the end, since again the rule can be applied to get even more! In fact, you now have an endless model!

  {g (a, g n + 1 (b)), g (b, g n + 1 (b))}

---

This right-to-left reading is often very useful when you are trying to understand recursive rules in Prolog. Reading from top to bottom (left to right) is often quite difficult, in particular, since you have to consider rollback and general unification.

Answer 2

Regarding your question:

"Also, since Herbrand models are a subset of the Herbrand base, how can I determine the smallest Herbrand model by induction?"

If you have a set of P horn sentences, a specific program, then you can define the program operator:

 T_P(M) := { HS | S is ground substitution, (H :- B) in P and BS in M } 

Smaller model:

 inf(P) := intersect { M | M |= P } 

Please note that not all models of a particular program are fixed points of the program operator. For example, the complete herbrand model is always a P program model, which shows that certain programs are always consistent, but this is not necessarily a fixed point.

On the other hand, each fixed point of a program operator is a model of a specific program. Namely, if you have T_P (M) = M, then we can conclude M | = P. So, after some further mathematical considerations (*), we can find that the smallest fixed point is also the smallest model:

 lfp(T_P) = inf(P) 

But we need some additional considerations so that we can say that we can determine the least model using some kind of computation. Namely, it is easy to notice that the program operator is continuous, i.e. preserves infinite union of chains, since the sentences of the horn do not have for all quantifiers in their body:

 union_i T_P(M_i) = T_P(union_i M_i) 

So, again, after some further mathematical reasoning (*), you can find that we can calculate the smallest fixed point through iteration, the witch can be used for simple induction. Each element of the smallest model has a simple derivation of the final Depth:

 union_i T_P^i({}) = lpf(T_P) 

Bye

(*) Most likely, you will find further hints on the exact mathematical reasoning needed in this book, but, unfortunately, I can’t remember which sections matter:
The Basics of Logical Programming, John Wiley Lloyd, 1984
http://www.amazon.de/Foundations-Programming-Computation-Artificial-Intelligence/dp/3642968287