Course for Graduate Students of the CIS department at University of Oregon

Planned schedules

• 25^th february at noon;
• 2^nd march at noon;
• 4^th march at noon;
• 9^th march at noon;
• 10^th march at noon;
• 11^th march at noon;
• 16^th march at noon.

Supporting Slides

The following slides are only supporting slides since most of the course is done on the board. Lecture Notes (see below) contain more complete material.

• (02/25/10) Introduction on Proof Systems (Hilbert Proof Systems, Deduction Theorem; Natural Deduction; Sequent Calculus, structural rules);
• (03/02/10) Gentzen's Hauptsatz for LK (Proof of the cut elimination theorem; intuitionistic sequent calculus LJ; Gödel translation);
• (03/04/10) Gödel's completeness theorem (One-sided sequents; Completeness theorem for first-order logic, in LK; Constructive theories)

Lecture Notes:

Coming soon...

Bibliography:

Here are listed several references (under construction):

• Proof and Types by Girard, Lafont and Taylor;
• Proof Theory and Automated Deduction, by Goubault-Larrecq and Mackie;
• ...