# INF551 - 2016 Exam

The duration of the exam is 3 hours.
There are 4 exercises.
To have full points at this exam you must do 3 of them, up to your choice.

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

At the end of the three hours,
hand in your paper for Exercise 1,
and send me by email (stephane.lengrand@polytechnique.edu) the files that you produced for Exercises 2, 3, 4.

Please WAIT until I have received your email before leaving the room.
## Exercise 1 - Pen and paper, Exercise 2 - Prolog

These two exercises are about decidability of intuitionistic propositional logic.
Exercise 2 can be done without having answered the questions of Exercise 1.

Download the file ex4.pdf.

Write up your answers to the three questions of Exercise 1 on paper.

Implement a decision procedure for intuitionistic propositional logic,
according to the three questions of Exercise 2.

## Exercise 3 - OCaml

This exercise consists in implementing the resolution method for classical propositional logic.

Download the file resolution.ml and open it in your favorite editor.
You may find it useful to also download
the mli file resolution.mli to see the type of those functions being provided and those functions you need to implement.

Follow the instructions in the comments of resolution.ml

You can test your program using the tests suite at the end.
All 6 tests should succeed, although the third one and the sixth one may take a lot of time, depending on how your implemented the algorithm.
If those two tests do not terminate, it does not mean that your code is incorrect and that you will not get any points.

## Exercise 4 - Coq

This exercise is about (a fragment of) the Zermelo Frankel set theory,
which we have seen in
Lecture 6.
We formalise the axioms in Coq, and build basic constructs from them.

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