This page will be continuously updated. Watch this webpage:
www2.math.uu.se/~palmgren/tillog/schema02.html
Lectures will take place in room 1145, unless otherwise
indicated.
| # | Time | Planned content (lecturer) | Material covered |
| week 36: 2-7/9 | |||
| 1 | Mo. 13.15-15.00 | Introductory lecture (LHE) | |
| 2 | Tu. 8.15-10.00 | Logical languages. Definability, decidability, undecidability (EP) | Oavgörbara problem i elementär aritmetik |
| 3 | Th. 8.15-10.00 | Non-constructive proofs. Typed lambda-calculus. Algorithmic interpretation of logical connectives. (EP) | Konstruktiv logik, ch 1-3. |
| 4 | Fr. 13.15-15.00 (room 1113) |
Exercise class (FD) | Exercises 1 |
| week 37: 9-14/9 | |||
| 5 | Mo. 10.15-12.00 | Intuitionistic logic. BHK-interpretation. Relation to classical logic. (EP) | Konstruktiv logik, ch 2-4. Ch 6 is cursory reading. |
| 6 | Tu. 8.15-10.00 | Possible worlds semantics. Modal logic. Soundness of intuitionistic logic. (EP) | Konstruktiv logik, ch 9. |
| 7 | Th. 8.15-10.00 | Temporal logic and transition systems (LHE) | Model-checking, pages 27-33 |
| 8 | Fr. 13.15-15.00 | Exercise class (FD) | Exercises 2 |
| week 38: 16-20/9 | |||
| 9 | Mo. 8.15-10.00 | Type-theory. Pi- and Sigma-types. Logical frameworks. (EP) | Konstruktiv logik, ch 7-8. |
| 10 | Tu. 8.15-10.00 | Logical frameworks. (EP) | Konstruktiv logik, ch 7-8. |
| 11 | Th. 9.15-12.00 (Room 4408) |
Laborative work in Agda/Alfa (EP) | |
| 12 | Fr. 13.15-15.00 | Discussion of Agda formalisations. Equational proofs and Birkhoff's completeness theorem. (EP) | Handout: section 1.1-1.2 |
| week 39: 23-27/9 | |||
| 13 | Mo. 10.15-12.00 | Sequent calculus, and its completeness as termination of proof search. (FD) | Sigstam: Fullständighetssatsen ... |
| 14 | Tu. 8.15-10.00 | Unification. Term rewriting. (EP) | Handout: section 1.2. Klop: Term rewriting systems. |
| 15 | Th. 10.15-12.00 (room 1212) |
Completeness (cont.) Decidable and undecidable teories. (EP) | van Dalen: Logic and structure. |
| 16 | Fr. 10.15-12.00 | Exercise class (FD) | |
| week 40: 30/9-4/10 | |||
| 17 | Mo. 13.15-15.00 | Resolution. (EP) | Das: Deductive databases and logic programming. |
| 18 | Tu. 10.15-12.00 | Decidable and undecidable teories (cont.) Quantifier elimination. (EP) | |
| 19 | Th. 10.15-12.00 | Termination proofs. Wellorderings and well-quasi orders (EP) | |
| 20 | Fr. 13.15-15.00 (room 1113) |
Exercise class (FD) | |
| week 41: 7-11/10 | |||
| 21 | Mo. 13.15-15.00 | Model checking safety properties (PA) | |
| 22 | Tu. 15.15-17.00 (Room 1146) |
Termination proof for model checking (PA) | |
| week 42: 14/10- | |||
| 23 | Mo. 13.15-15.00 | Exercise class (FD) |
Tentamen (Exam): 17 October.
PA = Parosh Abdulla, LHE = Lars-Henrik Eriksson (guest lecturers)
FD = Fredrik Dahlgren (assistant)