Department of Mathematics
Applied Logic (Tillämpad Logik)
No retake exam on 18 August, since no one registered.
The course starts on Friday, September 4, 10.15 in Room 2:214 (MIC,
Polacksbacken). The schedule may be found
Syllabus of course in English and in
A more detailed planning will be available
at the beginning of the course. Links to earlier
versions of the course can be found here:
Lectures and Exercise Classes
Lectures and exercises by Erik Palmgren (EP) and Anton Hedin (AH).
Approximately every third session will be an exercise class, where
solutions to set problems are presented and discussed.
- Lecture 1 (Sept. 4, EP): Introduction. First order logic and its
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.
- Lecture 4 (Sept. 14, EP ): Constructive logic and type theory
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
- 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,
- Lecture 8
(Sept. 28, EP): Automatic theorem proving (cont.) Exercise sheet 3 with bonus problems
- 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
- 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)
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,
Obligatory assignments: laboratory work
The first laboratory exercise will use the proof assistant Coq which is
available for downloading
here or there.
It should also be possible to work using the ProofWeb interface for Coq.
- A tutorial (G. Huet, G. Kahn, C. Paulin) is available
A quick introduction to Coq (Y. Bertot) with exercises is available
The problems are the following. They may be solved in groups
consisting of up to three persons.
- Laboratory assignment 1. Deadline
[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.
1. Obligatory assignments. This will involve of use
computers to do formal proofs.
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
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
December 8, 2009,