Clausal logic and resolution: theoretical backgrounds

12.2. Clausal logic and resolution: theoretical backgrounds#

Solution 2.1 #

Translate the following statements into clauses, using the atoms person, sad and happy:

persons are happy or sad;
no person is both happy and sad;
sad persons are not happy;
non-happy persons are sad.

The statements should be read as ‘if … then …’ statements. Thus, the first statement reads ‘if somebody is a person, then she is happy or sad’:

happy;sad:-person.

The second statement reads ‘if somebody is a person, then she is not both happy and sad’. In clausal logic, only positive conclusions can be drawn; negative conclusions are turned into positive conditions, as follows: ‘if somebody is a person, and she is happy and sad, then contradiction’. A contradictory conclusion is signalled by the empty head:

:-person,happy,sad.

Following the same recipe, the third statement expresses that ‘if somebody is a person who is sad, and she is happy, then contradiction’:

:-person,sad,happy.

Thus, sentences 2 and 3 convey the same logical meaning.

Finally, the fourth sentence reads ‘if somebody is a person who is not happy, then she is sad’. In clausal logic, only positive conditions can be used; therefore, this negative condition should be turned into a positive conclusion: ‘if somebody is a person, then she is sad or happy’. We thus obtain the same clause as in case 1:

sad;happy:-person.

Solution 2.2 #

Given the program

married;bachelor:-man,adult.
man.
:-bachelor.

determine which of the following clauses are logical consequences of this program:

married:-adult;
married:-bachelor;
bachelor:-man;
bachelor:-bachelor.

Any model of the first clause, which additionally makes man true, is also a model of the clause married;bachelor:-adult. Likewise, any model of this clause which additionally makes bachelor false is also a model of the clause married:-adult, which is therefore a logical consequence of the program.
The body of this clause is false in any model of the program, and therefore the clause is true in any such model.
The body of this clause is true in any model of the program, while its head is false. The clause is therefore not a logical consequence of the program (on the contrary, it is false in every model of the program, not just in some).
This clause is a tautology: it is true in any interpretation, and therefore a logical consequence of any program.

Solution 2.3 #

Write down the six Herbrand interpretations that are not models of the program

married;bachelor:-man,adult.
has_wife:-man,married.

The six interpretations are:

{ man, adult }
{ man, adult, has_wife }
{ man, married }
{ man, married, adult }
{ man, married, bachelor }
{ man, married, adult, bachelor }

The first two interpretations satisfy the body of the first clause but violate its head; the remaining four interpretations satisfy the body of the second clause but violate its head.

Solution 2.4 #

Give a derivation of friendly from the following program:

happy;friendly:-teacher.
friendly:-teacher,happy.
teacher;wise.
teacher:-wise.

This requires derivations of the clauses friendly:-teacher and teacher:

Notice that this derivation can not be recast in the form of a linear tree, where each resolvent is obtained from the previous resolvent and a given clause, as in Chapter 1. This is due to the fact that some clauses are indefinite (have more than one positive literal).

Solution 2.5 #

Prove by refutation that friendly:-has_friends is a logical consequence of the following clauses:

happy:-has_friends.
friendly:-happy.

The negation of friendly:-has_friends consists of two clauses, :-friendly and has_friends. Together, these four clauses are inconsistent:

Solution 2.6 #

How many models does the following clause have over the Herbrand universe {peter,maria}:

likes(peter,S):-student_of(S,peter).

The set of ground instances of this clause is

{ likes(peter,maria):-student_of(maria,peter),
  likes(peter,peter):-student_of(peter,peter) }

and the Herbrand base is

{ likes(peter,peter),      likes(maria,peter),
  likes(peter,maria),      likes(maria,maria),
  student_of(peter,peter), student_of(peter,maria),
  student_of(maria,peter), student_of(maria,maria) }

Only the four ground atoms in the left column are relevant for determining whether an interpretation is a model. 9 out of 16 truth-value assignments to these ground atoms result in a model. Because of the 4 irrelevant ground atoms, this yields \(9*2^4=144\) models. Notice that this is a rather large number of models for such a modest Herbrand universe, and such a simple clause! This illustrates that less knowledge leads to more models.

Solution 2.7 #

Write a clause expressing that Peter teaches all the first-year courses, and apply resolution to this clause and the clause

likes(peter,maria):-follows(maria,C),teaches(peter,C).

This is expressed by the clause

teaches(peter,C):-first_year_course(C).

Resolution with the above clause yields

likes(peter,maria):-follows(maria,C),first_year_course(C).

In words: ‘Peter likes Maria if Maria follows a first-year course’.

Solution 2.9 #

Translate to clausal logic:

every mouse has a tail;
somebody loves everybody;
every two numbers have a maximum.

This statement should be read as ‘if X is a mouse, then there exists something which is X’s tail’. Giving X’s tail the abstract name tail(X), we obtain the following clause:
```
tail_of(tail(X),X):-mouse(X).
```
Here we need to give the person who loves everybody an abstract name. Since this person does not depend on anybody else, it can simply be a constant:
```
loves(person_who_loves_everybody,X).
```
Notice the difference with the statement ‘everybody loves somebody’:
```
loves(X,person_loved_by(X)).
```
This statement should be read as ‘if X and Y are numbers, then there exists a number which is their maximum’. Giving this maximum the abstract name max(X,Y) yields the clause
```
maximum(X,Y,max(X,Y)):-number(X),number(Y).
```

Solution 2.10 #

Determine the Herbrand universe of the following program:

length([],0).
length([X|Y],s(L)):-length(Y,L).

(Hint: recall that [] is a constant, and that [X|Y] is an alternative notation for the complex term .(X,Y) with binary functor ‘.’!)

In the intended interpretation, s is restricted to numbers and ‘.’ is restricted to lists; however, variables are untyped in clausal logic, and the two sets of terms may be mixed. Thus, the Herbrand universe will contain terms denoting numbers, such as

0,s(0),s(s(0)),s(s(s(0))),…

and terms denoting lists of numbers, such as

[],[0],[s(0),0],[s(s(0)),s(0),0],…

but also ‘strange’ terms like

[[[0]]] or .(.(.(0,[]),[]),[])
[s(0)|0] or .(s(0),0)
[s([[]|0])]

and so on.

Solution 2.11 #

If possible, unify the following pairs of terms:

plus(X,Y,s(Y)) and plus(s(V),W,s(s(V)));
length([X|Y],s(0)) and length([V],V);
larger(s(s(X)),X) and larger(V,s(V)).

plus(s(V),s(V),s(s(V))).
length([s(0)],s(0)).
Not unifiable.

Solution 2.13 #

Write a clause for the statement ‘somebody is innocent unless proven guilty’, and give its intended model (supposing that john is the only individual in the Herbrand universe).

The clause is

innocent(X):-not guilty(X).

with intended model { innocent(john) }.

Solution 2.14 #

Translate to clausal logic:

\( \forall \texttt{X} \exists \texttt{Y} : \texttt{mouse(X)} \rightarrow \texttt{tail_of(Y,X)} \);
\( \forall \texttt{X} \exists \texttt{Y} : \texttt{loves(X,Y)} \land ( \forall \texttt{Z} : \texttt{loves(Y,Z)} ) \);
\( \forall \texttt{X} \forall \texttt{Y} \exists \texttt{Z} : \texttt{number(X)} \land \texttt{number(Y)} \rightarrow \texttt{maximum(X,Y,Z)} \).

This statement translates almost immediately into a clause, replacing the existential quantifier by a Skolem functor tail:
```
tail_of(tail(X),X):-mouse(X).
```
This formula is already in conjunctive normal form, and each conjunct yields a separate clause. After replacing the existential quantifier by a Skolem functor person_loved_by, we obtain
```
loves(X,person_loved_by(X)).
loves(person_loved_by(X),Z).
```
Notice that the two clauses are ‘linked’ by the Skolem functor.
Here, the Skolem functor has two arguments:
```
maximum(X,Y,max(X,Y)):-number(X),number(Y).
```
See also Exercise 2.9.