UPPSALA UNIVERSITY
Department of Mathematics

Fall 2009

Applied Logic (Tillämpad Logik)

General Information

  • 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 here.
  • Course information
  • Syllabus of course in English and in Swedish.
  • A more detailed planning will be available at the beginning of the course. Links to earlier versions of the course can be found here: 2000, 2001, 2002, 2004, 2006, 2007, 2008.

    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.
    1. 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.
    2. Lecture 2 (Sept. 7, EP): Undecidable problems: halting problem, PCP, truth in first order arithmetic.
    3. Exercise class (Sept. 9, EP): Solutions to bonus problems are to be presented. The ProofWeb system.
    4. Lecture 3 (Sept. 11, EP): Constructive logic and type theory. Lectures notes.
    5. 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.
    6. Exercise class (Sept. 16, EP)
    7. Lecture 5 (Sept. 18, EP): Constructive logic and type theory (cont.) Obligatory Laboratory assignment 1 handed out; see below.
    8. Lecture 6 (Sept. 21, EP): Constructive logic and type theory (cont.)
    9. Exercise class (Sept. 23, EP): Supervised laboratory exercise. (Please bring laptops with Coq installed.)
    10. 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)
    11. Lecture 8 (Sept. 28, EP): Automatic theorem proving (cont.) Exercise sheet 3 with bonus problems handed out.
    12. 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.
    13. 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.
    14. Lecture 11 (Mon Oct 26, AH): Semantics for intuitionistic propositional logic (contd.): Heyting algebras and Kripke semantics.
    15. Exercise class (Wed Oct 28, AH):
    16. Lecture 12 (Mon Nov 2, AH): Modal logic: Syntax and semantics of basic modal logic. Frame correspondence and engineering of modal logics.
    17. 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.
    18. Exercise class (Wed Nov 11, AH):
    19. Lecture 14 (Mon Nov 16, AH): Computation Tree Logic: syntax, semantics, examples. The labelling algorithm.
    20. Lecture 15 (Mon Nov 23): Guest Lecturer: Jesper Carlström from Prover.
    21. Exercise class (Wed Nov 25, AH):
    22. Lecture 16 (Mon Nov 30, AH): The fixed-point characterisation of CTL. Binary Decision Diagrams. Symbolic model checking. Bisimulation. Exercise sheet 6.
    23. Lecture 17 (Mon Dec 7, AH): CTL (contd.) and repetition.
    24. Exam (Wed Dec 16)

    Supplementary reading

    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.

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

    1. 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.]
    2. Laboratory assignment 2. Deadline January 20, 2010.

    Examination

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

    Teachers

    Some Links

    December 8, 2009, Erik Palmgren.