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:

You ARE NOT ALLOWED to:

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.