Herbrand in Prolog

Question

I was watching some issues such as Logica fuzzy logic and Horn clauses and saw some simple applications examples of them , with Prolog.

The reason for this question is because these issues are also among the Herbrand theorem which I consider a little more complicated than others, at least for me , and I had difficulty finding an application example related to Prolog .

That's why I wanted to provide me some applicative examples using Prolog , not so basic (because that generates the Herbrand model , according to the definition , are basic rules and always find this application example when search about Herbrand ) , for exclusive use Herbrand. Thanks

This is a example applicative code in Prolog:

p(f(X)):- q(g(X)).
p(f(X)):- p(X).
p(a).
q(b).

Answer 1

A set of clauses has a model iff it has a Herbrand model.

To prove that clause C is a consequence of clauses Cs, simply show that Cs∪~C is unsatisfiable.

This is, in abstract terms, what Prolog does, via a special case of resolution: You can regard the execution of a (pure—what else) Prolog program as the Prolog engine trying to find a resolution refutation of the negated query.

The form of resolution that Prolog implements, SLD resolution with depth-first search, does not guarantee though that all unsatisfiable clauses are disproved, it is incomplete.

In Prolog, procedural properties may impact the derivation of consequences. For example, with your program:

?- p(X).
wating...

Whereas we simply reorder the clauses as:

q(b).
p(a).
p(f(X)):- q(g(X)).
p(f(X)):- p(X).

we get:

?- p(X).
X = a ;
X = f(a) ;
X = f(f(a)) .

Note though that many important declarative properties are indeed preserved in the pure and monotonic subset of Prolog. See logical-purity for more information.