Proving with Computer Assistance 2IMF15

Teacher

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

AUD 15 on Thursdays, hours 5-8, 13:45-17:30.

Prerequisites

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

Material

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 http://prover-pca.cs.ru.nl/new. For ProofWeb:
  1. Get a login, by sending a mail
  2. Go to http://prover-pca.cs.ru.nl/new
  3. Login to "Proving with Computer Assistance 2017"
  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!

Examination

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 20-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