The file herbrand.pl implements the semantical notions discussed in this chapter, such as Herbrand base, interpretation and model. For instance, you can use it to generate all Herbrand interpretations of a given list of clauses, and to check whether a given clause is a logical consequence of a given list of clauses. Have a look at the file and you will see that, although you may not yet understand all Prolog constructs used there, the Prolog definitions follow the definitions given in the lectures fairly closely.
To use these programs, you have to specify which predicates, constants and functors there are in your language. Example propositional/relational/full clausal languages are given in the files prop.pl, rel.pl, and full.pl. Loading one of these files will automatically load herbrand.pl. You will also need the files library.pl and aux_sicstus.pl.
The following query can be used to generate the Herbrand models of the program in Exercise 2.2 (p.20):
?- herbrand_model([(bachelor;married:-man,adult),(man:-true),(false:-bachelor)], M).Note:
To check that married:-adult is a logical consequence of this program you can use the query
?- logical_consequence((married:-adult), [(bachelor;married:-man,adult),(man:-true),(false:-bachelor)], Answer). Answer = yesIn case the clause given as the first argument is not a logical consequence of the program given as second argument, this program returns a countermodel (a model of the program that is not a model of the clause):
?- logical_consequence((bachelor:-man), [(bachelor;married:-man,adult),(man:-true),(false:-bachelor)], Answer). Answer = countermodel([man])Notice that, because of the 'hidden' cut in the ( if -> then ; else ) construct (Section 3.4 of the book), this program stops with the first countermodel it finds, and cannot be used to generate all countermodels.
?- herbrand_model([...],M). M = [woman] ? ; M = [man] ? ; M = [adult,woman] ? ; M = [adult,married,woman] ? ; M = [adult,man,married] ? ; M = [adult,bachelor,man] ? ; noHint: this requires 7 clauses, all of which are true (more or less) in the actual world.
According to the answer to Exercise 2.6 (p.215) the clause likes(peter,S):-student_of(S,peter) has 144 models (check the calculation, and verify by means of a query!). We are going to reduce the number of models by adding information.
adult:-married. man.but the following does not (check!):
married;bachelor:-man,adult. adult:-married. man.
Find out which of the following programs has the model intersection property:
man:-bachelor. adult:-bachelor. bachelor.
man:-bachelor. adult:-bachelor. married;bachelor.
man:-bachelor. adult:-bachelor. :-married.
Actually you should have known better, since the Herbrand base of a full clausal langauge is infinite! Check this by asking for a few solutions to the query ?-ground_term(T). and ?-ground_atom(A). As a consequence, none of the predicates herbrand_interpretation, herbrand_model and logical_consequence will terminate, since they all generate interpretations from the Herbrand base.
If we modify the program a little bit, we can however continue to check whether a clause is true in an interpretation. Consider the following definition of false_clause:
false_clause((false:-Body),I):- ground_clause((false:-Body)), true_body(Body,I). false_clause((Head:-Body),I):- ground_clause((Head:-Body)), true_body(Body,I), not true_head(Head,I).The problem is that ground_clause may generate an infinite number of substitutions before hitting on a falsifying one. However, any variables in the body of the clause will also be ground by the call true_body(Body,I). So if we make sure that we don't test clauses with head variables that do not occur in the body, we may remove the calls to ground_clause.