Proving with Computer Assistance 2IMF15


Herman Geuvers: home page
Room number MF6.079A (only on Thursdays) For contact, use the e-mail address herman at cs dot ru dot nl

Location and time

Thursdays, hours 5-6, L1.105 and hours 7-8, V7.08.


We assume that you are familiar with a bit of logic, especially natural deduction and (untyped) lambda calculus.


System we will use

We will be using the Proof Assistant Coq in this course. You can download and install Coq locally, but you can also use it through the ProofWeb webinterface at (NB: ProofWeb runs Coq version 8.3.pl4, the latest version that works smoothly with the web interface. A Coq version you download and install yourself will most likely be more recent.)

For ProofWeb:

  1. Get a login, by sending a mail
  2. Go to
  3. Login to "Proving with Computer Assistance 2018"
  4. Load one of the files (preferably start with the proposition_logic.v file)
  5. You can now type in tactics to create proofs in natural deduction. You can also select these from the Templates menu.
  6. Check "Fitch style natural deduction" in the Display menu, to see the proofs in Fitch style.
  7. If you don't know what to do, load the file proposition_logic.v and "play" the proofs that are given there.

The course by week

This schedule may be subject to changes!


The mark for the course is determined by the 2 marks you will get for the two items listed below. Note that you don't receive a mark if you haven't completed all parts of the course. For the second chance ("Hertentamen"), all guidelines above apply with the following dates/deadlines:

Coq Assignments

Deadline: Thursday 19-04-2017; deliver your assignment by mail to the teacher.

Here is a page about the of Coq assignment. (Look here for some additional comments regarding the use of lists.) Options:

To complete the Coq assignment follow these steps:

A couple of remarks concerning the report:

Useful links

herman at cs dot ru dot nl