Proving with Computer Assistance 2IMF15

!! Exam consultation that is: you can see your graded work, on Thursday 2-05-2019, 15:00- 16:00 in MF6.079A !!


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: ATLAS -1.825 and hours 7-8, Gemini-Zuid Collegezaal (lecture hall).


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 2019"
  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 (so I will write "NV") 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 11-04-2019; do the assignment in couples 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