INF551 - 2015 Exam

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



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:

Download the file 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:

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

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 :

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 :

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.