# Clausal logic and resolution: theoretical backgrounds

# 12.2. Clausal logic and resolution: theoretical backgrounds¶

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.
```

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.

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.

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).

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:

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(peter,maria),
likes(maria,peter), likes(maria,maria),
student_of(peter,peter), student_of(peter,maria),
student_of(maria,peter), student_of(maria,maria) }
```

Only the left four ground atoms 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*.

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’.

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 clausemaximum(X,Y,max(X,Y)):-number(X),number(Y).

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.

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.

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) }`

.

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 obtainloves(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.