Applied Logic (Tillämpad Logik)

News

General information

• Syllabus of course in English and in Swedish.
• Course information
• This page will be updated regularly.
• Links to earlier versions of the course can be found here: 2000, 2001, 2002, 2004, 2006, 2007.

Lectures

1. Lecture 1 (Sept. 8, EP): Introduction. Incompleteness. Undecidable problems: halting problem, PCP, truth in first order arithmetic.
2. Lecture 2 (Sept. 11, EP): Undecidable problems: halting problem, PCP, truth in first order arithmetic (cont.)
3. Exercise class (Sept. 16, AH).
4. Lecture 3 (Sept. 18, EP): Satisfiability problem for propositional logic. Methods for Horn formulas and 2-CNF. Stålmarcks method. (Huth and Ryan Ch 1.5-1.6.)
5. Lecture 4 (Sept. 22, EP): Satisfiability problem for propositional logic (cont.). Efficient representation of propositional formulas. Binary Decision Diagram (BDD).
6. Exercise class (Sept 25, AH)
7. Lecture/Exercise (Sept 29, AH)
8. Lecture/Exercise (Oct 2, AH)
9. Lecture/Exercise (Oct 9, AH)
10. Lecture/Exercise (Oct 13, AH)
11. Lecture/Exercise (Oct 20, AH)
12. Lecture/Exercise (Oct 23, AH)
13. Seminar (Oct 30) Jonathan Cederberg: Infinite state systems.
14. Lecture (Nov 3, EP)
15. Lecture (Nov 6, EP)
16. Lecture (Nov 10, EP)
17. Exercise class (Nov 13, AH)
18. ..
19. ..
20. ..
21. ..
22. ..
23. ..
24. ..

Hand-outs

• Bjorn Poonen, Undecidability in Number Theory, Notices of the American Mathematical Society 55(2008) no. 3, 344-350. Study pages 344-346.
• Satisfibility for 2-CNF formulas.
• Erik Palmgren, Constructive logic and type theory. Lecture notes, Uppsala University 2004.
• Anton Hedin, Modal Logic, Lectures notes.
• Equational logic, unification and term rewriting. (Lecture notes, E. Palmgren)
• Some logical background to the resolution method. (Lecture notes, E. Palmgren)
• ...

Supplementary reading

• ...

Exercises

• Exercises 1 --- Sept. 16
• Exercises 2
• Exercises in Modal Logic. Solutions.
• Exercises 3 --- -- --Nov. 13. Solution (Anton H) to exercise 3.12.
• Exercises 4 --- Dec. 4
• ...

Laboratory work

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

1. Laboratory Exercise, Part 1. Deadline 4 December. 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 Exercise, Part 2. Deadline 18 December.

Examination

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.

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

Teachers

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

Links

• The Stockholm-Uppsala Logic Seminar, Wednesdays at 10.00 or 10.30.
• Seminar on Theories of Proofs, Types and Computation.
• 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.