Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Herbrand universe and Least herbrand Model

I read the question asked in Herbrand universe, Herbrand Base and Herbrand Model of binary tree (prolog) and the answers given, but I have a slightly different question more like a confirmation and hopefully my confusion will be clarified.

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

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

From the above program, the Herbrand Universe

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))...e.t.c}

Herbrand base:

Bp = {q(s, t) | s, t E Up}
  • Now come to my question(forgive me for my ignorance), i included q(a, g(a)) as an element in my Herbrand Universe but from the fact, it states q(a, g(b)). Does that mean that q(a, g(a)) does not suppose to be there?
  • Also since the Herbrand models are subset of the Herbrand base, how do i determine the least Herbrand model by induction?

Note: I have done a lot of research on this, and some parts are well clear to me but still i have this doubt in me thats why i want to seek the communities opinion. Thank you.

like image 908
Plaix Avatar asked Jan 27 '14 15:01

Plaix


1 Answers

From having the fact q(a,g(b)) you cannot conclude whether or not q(a,g(a)) is in the model. You will have to generate the model first.

For determining the model, start with the facts {q(a,g(b)), q(b,g(b))} and now try to apply your rules to extend it. In your case, however, there is no way to match the right-hand side of the rule q(X,g(X)) :- q(X,g(g(g(X)))). to above facts. Therefore, you are done.

Now imagine the rule

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

This rule could be used to extend our set. In fact, the instance

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

is used: If q(b,g(b)) is present, conclude q(a,g(g(b))). Note that we are using here the rule right-to-left. So we obtain

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

thereby reaching a fixpoint.

Now take as another example you suggested the rule

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

Which permits (I will no longer show the instantiated rule) to generate 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 produce even more! In fact, you have now an infinite model!

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

This right-to-left reading is often very helpful when you are trying to understand recursive rules in Prolog. The top-down reading (left-to-right) is often quite difficult, in particular, since you have to take into account backtracking and general unification.

like image 124
false Avatar answered Nov 10 '22 13:11

false