Simply Logical lab exercises chapter 2

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

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.

Consult prop.pl. 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).
```
Note:
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),
                       [(bachelor;married:-man,adult),(man:-true),(false:-bachelor)],
                       Answer).
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),
                       [(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.
- Add a propositional atom woman to the language, and check that the Herbrand base is now enlarged. Express in clausal logic "somebody is a woman if and only if she is not a man" (2 clauses) and demonstrate that in each model of these two clauses exactly one of man/woman is true by listing all answers to the query ?-herbrand_model([...],M).
- Find a list of clauses that has exactly the following models:
```
?- herbrand_model([...],M).
M = [woman] ? ;
M = [man] ? ;
M = [adult,woman] ? ;
M = [adult,married,woman] ? ;
M = [adult,man,married] ? ;
M = [adult,bachelor,man] ? ;
no
```
  Hint: this requires 7 clauses, all of which are true (more or less) in the actual world.
Consult rel.pl. 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.
- Express in clausal logic (1 clause each):
  1. Everybody likes him/herself.
  2. Nobody is a student of him/herself.
  3. Peter is a student of nobody.
- Now, determine all models of these 4 clauses (incl. the one above).
  NB. When checking this by means of the program herbrand_model, you should make sure that no variables occur in more than one clause.
- Finally, determine whether "nobody is a student of Maria" is a logical consequence of these clauses.
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!):
```
   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:
1. ```
   man:-bachelor.
   adult:-bachelor.
   bachelor.
```
2. ```
   man:-bachelor.
   adult:-bachelor.
   married;bachelor.
```
3. ```
   man:-bachelor.
   adult:-bachelor.
   :-married.
```
4. ```
   man:-bachelor.
   adult:-bachelor.
```
Consult full.pl. 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:
```
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.
- Make this modification, and then check which of the following clauses is true in the interpretation {plus(0,0,0), plus(0,s(0),s(0), plus(s(0),0,s(0)}:
  1. plus(s(X),Y,s(Z)):-plus(X,Y,Z).
  2. plus(X,Y,Z):-plus(s(X),Y,s(Z)).
  3. :-plus(X,X,s(X)).
  For each clause that is false in the given interpretation, give a ground instance that is false.

Back / Peter Flach