The duration of the exam is 2 hours. There are 4 exercises. They are independent and of equal value.

You ARE ALLOWED to:

- consult any document (all are allowed, including electronic ones);
- go on the internet, e.g. to look for documentation (especially regarding libraries), although it should be possible to do the exercises without doing so;
- use any of the libraries available on your laptop (but please indicate them in your file header).

- copy and paste code from the internet
- communicate with people during the 2 hours

In lecture 4 you have seen Robinson's unification algorithm. The unification problem determines if, given two terms t1 and t2, there exists a substitution σ such that σ(t1) = σ(t2). The algorithm processes a list of equations (starting with the list [t1;t2] containing the first two terms) and the rules of the algorithm, as shown in class, are the following:

- (t = t)::ls → ls
- (f(t1,..,tn) = f(u1,..,un))::ls → (t1 = u1)::..::(tn = un)::ls
- (x = t)::ls and x not featured in t → σ(ls) where σ is the substitution (x->t). In case that solving σ(ls) returns a substitution τ, then return σ•τ (where • is composition)
- (f(t1,..tn) = g(u1,..,um))::ls if f ≠ g → fail
- (x = t)::ls and x featured in t, t distinct from x → fail

The file starts with the definitions of terms, for example
```
Term ("f", [Var "x"; Term ("a",[])])
```

represents the term f(x,a).

The main algorithm processes a list of equations, according to the above rules, and returns an optional substitution:

- An equation is denoted using the
constructor
`Eq`

from type`eq`

, for example`Eq (t1, t2)`

represents the equation t1 = t2. -
A substitution is a function of type
`string -> fol`

`unify_list`

, of type
```
eq list -> (string -> fol) option
```

:
it should return `Some substitution`

if the terms are unifiable (with most general unifier `substitution`

), and `None`

otherwise.
For this it may be useful to implement the auxiliary functions proposed in `unif.ml`

Your function will be called in the final wrapper ```
unify:
fol -> fol -> (string -> fol) option
```

, unifying two terms.

You can test your program using the tests suite at the end. All four tests should succeed.

`unif.ml` :

In this exercise you will help a group of people cross a river.

The group consists of adults and of children, which all arrive on the left bank of a river.
Luckily, there is a boat on the bank which they can use to move to the other side.
Unfortunately, the boat can take each time at most two children or one adult.

Both adults and children can navigate the boat.

We will use a list to denote the location of each member of each of the two groups of people.
For example, if two adults are on the left bank and one is on the right one, it can be denoted by
the list ` [r,l,l] `

.

The same goes for the group of children. We also need to keep track of the location
of the boat and therefore we will use the following list
` [Boat,AdultsGroup,ChildrenGroup] `

to denote a state of the problem.
Initially, the boat and all members of the groups are on the left bank. For example
if we have 2 adults and 3 children, the starting state is ` [l,[l,l],[l,l,l]] `

.

Implement the predicate ` solve(S,X) `

such that ` X `

denotes a list describing all the intermediary states required to reach the right bank when
starting from the initial state S. For the above example, we will have
` X = [[r,[r,r],[r,r,r]],...,[l,[l,l],[l,l,l]]]`

.

`puzzle.pl` :

This exercise is about Binary Search Trees (you do not need to read the page to do the exercise, though). We formalise them in Coq, and prove properties about them.

`BST.v`:

This exercise is about resolution.