Simply Logical lab exercises chapter 2

The exercises are about models for propositional, relational and full clausal logic.

The file 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,, and Loading one of these files will automatically load You will also need the files and

  1. Consult This defines a propositional clausal language. Check which one by means of the query ?-herbrand_base(B).

    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).
    1. we need brackets around the clauses because of overloading of ':-', ';' and ','
    2. the empty body is represented by true and the empty head by false

    To check that married:-adult is a logical consequence of this program you can use the query

    ?- logical_consequence((married:-adult),
    Answer = yes
    In 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),
    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.

  2. Consult This defines a relational clausal language. Check which one by means of the query ?-herbrand_base(B).

    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.

  3. Since any subset of the Herbrand base is a Herbrand interpretation, the intersection of two Herbrand interpretations is also a Herbrand interpretation, assigning true to an atom just in case the original interpretations both assign true to it. We say that a program has the model intersection property if the intersection of any two of its models is also a model. For instance, the following program has the model intersection property (check!):
    but the following does not (check!):

    Find out which of the following programs has the model intersection property:

    1.    man:-bachelor.
    2.    man:-bachelor.
    3.    man:-bachelor.
    4.    man:-bachelor.

  4. Consult This defines a full clausal language. Check which one by means of the query ?-herbrand_base(B).

    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:

            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.

Back / Peter Flach