(apx:c.2)=
# Clausal logic and resolution: theoretical backgrounds #
```{solution} ex:2.1
```
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':
```Prolog
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:
```Prolog
:-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':
```Prolog
:-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:
```Prolog
sad;happy:-person.
```
+++
```{solution} ex:2.2
```
1. 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.
1. The body of this clause is **false** in any model of the program, and therefore the clause is **true** in any such model.
1. 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).
1. This clause is a *tautology*: it is **true** in any interpretation, and therefore a logical consequence of any program.
+++
````{solution} ex:2.3
Write down the six Herbrand interpretations that are not models of the program
```Prolog
married;bachelor:-man,adult.
has_wife:-man,married.
```
````
The six interpretations are:
```Prolog
{ 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} ex:2.4
```
This requires derivations of the clauses `friendly:-teacher` and `teacher`:
```{figure} /src/fig/appendices/image004.svg
---
width: 100%
name: 'fig:a.2'
---
```
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 {numref}`Chapter %s`. This is due to the fact that some clauses are indefinite (have more than one positive literal).
+++
```{solution} ex:2.5
```
The negation of `friendly:-has_friends` consists of two clauses, `:-friendly` and `has_friends`. Together, these four clauses are inconsistent:
```{figure} /src/fig/appendices/image006.svg
---
width: 45%
name: 'fig:a.3'
---
```
+++
````{solution} ex:2.6
How many models does the following clause have over the Herbrand universe `{peter,maria}`:
```Prolog
likes(peter,S):-student_of(S,peter).
```
````
The set of ground instances of this clause is
```Prolog
{ likes(peter,maria):-student_of(maria,peter),
likes(peter,peter):-student_of(peter,peter) }
```
and the Herbrand base is
```Prolog
{ 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*.
+++
````{solution} ex:2.7
Write a clause expressing that Peter teaches all the first-year courses, and apply resolution to this clause and the clause
```Prolog
likes(peter,maria):-follows(maria,C),teaches(peter,C).
```
````
This is expressed by the clause
```Prolog
teaches(peter,C):-first_year_course(C).
```
Resolution with the above clause yields
```Prolog
likes(peter,maria):-follows(maria,C),first_year_course(C).
```
In words: 'Peter likes Maria **if** Maria follows a first-year course'.
+++
```{solution} ex:2.9
```
1. 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:
```Prolog
tail_of(tail(X),X):-mouse(X).
```
1. 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:
```Prolog
loves(person_who_loves_everybody,X).
```
Notice the difference with the statement 'everybody loves somebody':
```Prolog
loves(X,person_loved_by(X)).
```
1. 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
```Prolog
maximum(X,Y,max(X,Y)):-number(X),number(Y).
```
+++
````{solution} ex:2.10
Determine the Herbrand universe of the following program:
```Prolog
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
```Prolog
0,s(0),s(s(0)),s(s(s(0))),…
```
and terms denoting lists of numbers, such as
```Prolog
[],[0],[s(0),0],[s(s(0)),s(0),0],…
```
but also 'strange' terms like
```Prolog
[[[0]]] or .(.(.(0,[]),[]),[])
[s(0)|0] or .(s(0),0)
[s([[]|0])]
```
and so on.
+++
```{solution} ex:2.11
```
1. `plus(s(V),s(V),s(s(V)))`.
1. `length([s(0)],s(0))`.
1. Not unifiable.
+++
```{solution} ex:2.13
```
The clause is
```Prolog
innocent(X):-not guilty(X).
```
with intended model `{ innocent(john) }`.
+++
```{solution} ex:2.14
```
1. This statement translates almost immediately into a clause, replacing the existential quantifier by a Skolem functor `tail`:
```Prolog
tail_of(tail(X),X):-mouse(X).
```
1. 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
```Prolog
loves(X,person_loved_by(X)).
loves(person_loved_by(X),Z).
```
Notice that the two clauses are 'linked' by the Skolem functor.
1. Here, the Skolem functor has two arguments:
```Prolog
maximum(X,Y,max(X,Y)):-number(X),number(Y).
```
See also {numref}`ex:2.9`.