UPPSALA UNIVERSITY Department of Mathematics | Fall 2009 |

- Lecture 1 (Sept. 4, EP): Introduction. First order logic and its
semantics. Incompleteness.
Exercise sheet 1 was handed out.
The
**bonus problems**on that sheet are here. The ProofWeb system. - Lecture 2 (Sept. 7, EP): Undecidable problems: halting problem, PCP, truth in first order arithmetic.
- Exercise class (Sept. 9, EP): Solutions to bonus problems are to be presented. The ProofWeb system.
- Lecture 3 (Sept. 11, EP): Constructive logic and type theory. Lectures notes.
- Lecture 4 (Sept. 14, EP ): Constructive logic and type theory
(cont.)
Exercise sheet 2 handed out. Note
that the solutions of the
**bonus problems**on this sheet are to be handed in on September 21. - Exercise class (Sept. 16, EP)
- Lecture 5 (Sept. 18, EP): Constructive logic and type theory (cont.)
Obligatory
**Laboratory assignment 1**handed out; see below. - Lecture 6 (Sept. 21, EP): Constructive logic and type theory (cont.)
- Exercise class (Sept. 23, EP): Supervised laboratory exercise. (Please bring laptops with Coq installed.)
- Lecture 7 (Sept. 25, EP): Proof search and automatic theorem proving. Hand-outs: Equational logic, unification and term rewriting. (Lecture notes, E. Palmgren) Some logical background to the resolution method. (Lecture notes, E. Palmgren)
- Lecture 8
(Sept. 28, EP): Automatic theorem proving (cont.) Exercise sheet 3 with
**bonus problems**handed out. - Lecture/Exercise class (Oct. 5, EP): Automatic theorem proving
(cont.) Presentation of solutions by students. Exercise sheet 4 with
**bonus problems**handed out. Deadline: October 26. -
Lecture 10 (Wed Oct 7, AH): The resolution method (contd.). Semantics for
intuitionistic propositional logic: Lattices and Boolean algebras.
Lecture notes. Exercise sheet 5 with
**bonus problems**handed out. Deadline: November 2. - Lecture 11 (Mon Oct 26, AH): Semantics for intuitionistic propositional logic (contd.): Heyting algebras and Kripke semantics.
- Exercise class (Wed Oct 28, AH):
- Lecture 12 (Mon Nov 2, AH): Modal logic: Syntax and semantics of basic modal logic. Frame correspondence and engineering of modal logics.
- Lecture 13 (Mon Nov 9, AH): Modal logic: More general modal languages. Some model theory - filtrations and bi-similations. Modal logic as a fragment of first order logic.
- Exercise class (Wed Nov 11, AH):
- Lecture 14 (Mon Nov 16, AH): Computation Tree Logic: syntax, semantics, examples. The labelling algorithm.
- Lecture 15 (Mon Nov 23): Guest Lecturer: Jesper Carlström from Prover.
- Exercise class (Wed Nov 25, AH):
- Lecture 16 (Mon Nov 30, AH): The fixed-point characterisation of CTL. Binary Decision Diagrams. Symbolic model checking. Bisimulation. Exercise sheet 6.
- Lecture 17 (Mon Dec 7, AH): CTL (contd.) and repetition.
- Exam (Wed Dec 16)

- P. Martin-Löf. Intuitionistic Type Theory. Notes by Giovanni Sambin. Bibliopolis 1984.
- On the meanings of the logical constants and the justifications of the logical laws. (P. Martin-Löf)
- Martin-Löf type theory (B. Nordström, K. Petersson, J.M. Smith)
- Programming in Martin-Löf type theory (B. Nordström, K. Petersson, J.M. Smith)
- Type Theory in Stanford Encyclopedia of Philosophy by Thierry Coquand.
- Wilfried Sieg, John Byrnes. Normal Natural Deduction Proofs (in classical logic). Studia Logica 60, 67-106, 1998.
- Wilfried Sieg, Saverio Cittadini. Normal Natural Deduction Proofs (in Non-classical logics). Mechanizing Mathematical Reasoning, LNAI 2605, 169-191, 2005.

- A tutorial (G. Huet, G. Kahn, C. Paulin) is available here.
- A quick introduction to Coq (Y. Bertot) with exercises is available here.

The problems are the following. They may be solved in groups consisting of up to three persons.

- Laboratory assignment 1. Deadline October 16. [Practical hints: example of use of the tactics "assert" and "contradiction", simplistic example of use of definitions and the tactics "fold", "unfold" and "red". Some examples of derivation involving ensembles.]
- Laboratory assignment 2. Deadline January 20, 2010.

2. A written examination at the end of the course.

Note: * You may bring along and use all course literature, all
hand-outs and all notes from the course during the written exam.*

3. It will be possible to earn ** bonus points ** by solving
certain set exercises and handing in the solutions or by presenting
solutions during the exercise classes. See details on the exercise
sheets in list of lectures above. The bonus points are added to the
score of the written exam, and can constitute up to 15 % of the
maximum score.

OLD EXAMS can be found here. Note: the course has changed several times, so not all problems may be relevant. The following problems are still relevant for this course

- 2000-10-20: 1-3,5,8
- 2001-10-17: 1-5,8
- 2002-01-16: 1-5,7,8
- 2002-10-17: 1-5,7,8
- 2003-01-15: 1-5
- 2004-05-26: 1-7
- 2006-06-07: 1-3, 5-7
- 2007-05-24: 1-7
- 2007-12-17: 1-8
- 2008-03-27: 1-8
- 2008-12-18: 1-8

- Professor Erik Palmgren. Examiner.
- Anton Hedin, Assistant, PhD student in mathematical logic.

- The Stockholm-Uppsala Logic Seminar.
- Alfa -- a graphical version of the Agda proof assistant.
- Agda - Official Web Site
- The Coq proof assistant
- Prover 9 -- an automated theorem prover for first-order and equational logic.
- Pesca -- a proof editor for sequent calculus.
- Haskell -- a purely functional language.

December 8, 2009, Erik Palmgren.