# INF551 - 2015 Exam

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).
You ARE NOT ALLOWED to:
• copy and paste code from the internet
• communicate with people during the 2 hours

## Exercise 1 - OCaml

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

Download the file unif.ml and open it in your favorite editor.

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 ```
Implement the function `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.

Upload the file unif.ml :

## Exercise 2 - Prolog

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

Upload the file puzzle.pl :

## Exercise 3 - Coq

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.

Download the file BST.v and follow the instructions in it.

Upload the file BST.v:

## Exercise 4 - paper question

This exercise is about resolution.

Download the file ex4.pdf and answer the questions on it.

Write up your answers on the official paper, and hand it to us at the end of the two hours.