Lectures and Exercise Classes

1. (Tu 31 Aug) General introduction. Formalization of logic and mathematics. Propositional logic and its encoding in Coq. vNatural deduction. Assumptions and contexts. Proof objects. Demonstration of the Coq system. Lecture notes.
2. (Th 2 Sept) Types, Predicates and Quantifiers. Predicate logic in Coq. Short laboratory exercise: if possible bring laptops with Coq/CoqIde installed. See Coq Tutorial. Laboratory assignment 1 is here.
3. * (Th 9 Sept) Some theoretical limits of automatic theorem proving. First order logic, completeness and incompleteness. Undecidable problems: halting problem, PCP, truth in arithmetic. Some important decidable problems.
4. (Fr 10 Sept) Typed lambda calculus and functional programming. Type checking. Computing in Coq. Another Coq Tutorial. Gödel's system T programmed in Coq.
5. (Tu 14 Sept) Brouwer-Heyting-Kolmogorov's constructive interpretation of logic. Constructive logic and type theory.
6. (We 15 Sept) Intuituinistic logic. Exercise class.
7. (Tu 21 Sept) Type theory. Dependent types. Formalization of mathematics in Coq.
8. (Th 23 Sept) Theories and tactics in Coq. Inductive types and definitions. Demonstration of Coq. Bring computers with Coq installed.
9. * (Fr 24 Sept) Brouwerian counter examples. Constructive logic and its relation to classical logic. Gödel-Gentzen negative interpretation.
10. (Mo 27 Sept) Equational logic and term rewriting. Notes. Using rewriting rules in Coq.
11. * (We 29 Sept) Seminar on Confluence of Term Rewriting Systems by Mizuhito Ogawa (JAIST), room 2214, 10.30-12.15. (Part of the Logic seminar.)
12. (Th 30 Sept) Unification. More about term rewriting.
13. (Th 5 Oct) Termination proofs. Well-founded sets and well-quasi orders.
14. (Tu 12 Oct) Recursive path order. Multiset order. Notes.
15. (Fr 29 Oct) Semantics of intuitionistic propositional logic. Heyting algebras and Kripke models. Lectures notes.
16. (Tu 2 Nov) Model checking. Linear-time Temporal Logic (LTL). Transition systems.
17. (We 3 Nov) The NuSMV model checker system. Computational Tree Logic (CTL). Labelling algorithms. The Sokoban transport puzzle. Java Sokoban.
18. (Th 4 Nov) Laboratory exercise (please bring computer with NuSMV installed and see the NuSMV Tutorial by Cavada et al.) LTL and CTL in comparison. CTL*.
19. (Mo 8 Nov) Basic modal logic. Embedding intuitionistic logic in modal logic.
20. (Tu 9 Nov) Reasoning about knowledge in modal logic. Binary Decision Diagram (BDD).
21. (Th 11 Nov) BDDs (cont.). Symbolic model checking. Some logical background to the resolution method.
22. (Fr 17 Dec): Extra lecture or exercise class.
23. December 21: written exam.

Assignments and Exercises

• Assignment 1 - Laboratory exercise in Coq. Some fair hints for the last problem. (Maximum score: 15 points)
• Assignment 2 - note only A-marked exercises are to be handed in. (Maximum score: 20 points)
• Exercises 3 - these are not assignments (so far).
• Assignment 3 - Laboratory exercise 2 in Coq. Some useful examples . (Maximum score: 15 points)
• Assignment 4 (Maximum score: 30 points)
• Assignment 5 (Maximum score: 30 points)
• Assignment 6 (Maximum score: 25 points)
• Assignment 7 (Maximum score: 30 points)

Course text and notes

• M.R.A. Huth and M.F. Ryan. Logic in Computer Science: Modelling and reasoning about systems. Second edition. Cambridge University Press 2004. Author's web page with auxiliary material.
• E. Palmgren. Constructive Logic and Type Theory. Lecture notes 2004.

Supplementary reading

• P. Martin-Löf. Intuitionistic Type Theory. Notes by Giovanni Sambin. Bibliopolis 1984. (Google the title and you can probably find a "bootleg copy" of this book.)
• 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.
• Jan Willem Klop. Term Rewriting Systems. Chapter 1 in Handbook of Logic in Computer Science, vol. 2, S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, eds., pages 1-117, Oxford University Press (1992).
• N. Dershowitz and J.-P. Jouannaud, Rewrite Systems.

Examination (Applied Logic)

1. Assignments. These will involve of use of computers to do formal proofs, as well ordinary mathematical problem solving. (70% of total score)

2. A short written examination at the end of the course (30% of total score). The written exam will have fewer technical questions than previous exams, since this is covered by assignments, but instead some more general questions about principles and methods.

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

Teacher

• Erik Palmgren.

Some Links

• The Coq proof assistant
• ProofWeb (Webbased version of Coq.)
• Rewriting Home Page
• Prover 9 -- an automated theorem prover for first-order and equational logic.
• Haskell -- a purely functional language.

  ---

• The Stockholm-Uppsala Logic Seminar.