| Subject |
Slides |
Notes |
| Introduction |
Slides 01 in color
Slides 01 in B/W |
- |
| Traditional Logic |
Slides 02 in color
Slides 02 in B/W |
Notes on Traditional Logic
Coq script used in lecture
Coq cheat sheet (v1)
Cheat sheet for traditional logic
|
| Induction and Propositional Logic |
Slides 03a in color (Induction)
Slides 03a in B/W (Induction)
Slides 03b in color (Propositional Logic)
Slides 03b in B/W (Propositional Logic) |
Notes on Induction
Coq script (induction) used in lecture
Notes on Propositional Logic
Coq script (propositional logic) used in lecture |
| Propositional Logic II; Predicate Logic I |
Slides 04a in color (Propositional Logic II)
Slides 04a in B/W (Propositional Logic II)
Slides 04b in color (Predicate Logic I)
Slides 04b in B/W (Predicate Logic I) |
Notes Propositional Logic II
Notes Predicate Logic I |
| Predicate Logic II |
Slides 05a in color (Predicate Logic II)
Slides 05a in B/W (Predicate Logic II)
Slides 05b (Insights into Coq proofs)
|
Notes Predicate Logic II
Coq script on variable scoping
Cheat sheet (explicit propositions vs builtin propositions)
Cheat sheet on predicate logic
|
| Induction; midterm |
midterm test (including solutions)
Coq script for midterm (Questions 8, 9 and 10)
(For practicing, take a look at
last year's midterm test, including solutions)
Slides 06 on induction (but the notes on induction given as suplementary reading in the next week are better)
|
-
|
An application of SAT solving
An application of theorem proving
Induction in Coq |
Slides 07a in color (Propositional Logic: Application of SAT Solving)
Slides 07a in B/W (Propositional Logic: Application of SAT Solving)
Slides 07b in color (Application of predicate logic and increasing trustworthiness)
Coq script on induction
|
Notes on formal induction
|
| Modal Logic I
| Slides 08 in color
Slides 08 in B/W
|
Notes on Modal Logic I |
| Modal Logic II
| Slides 09 in color
Slides 09 in B/W
|
Notes on Modal Logic I (including Coq)
Coq script on Modal Logic I |
| Program verification I |
Slides 10 in Color (Program verification I)
|
Notes on Hoare Logic (covering I and II, updated)
|
| Program verification II |
Slides 11a in Color (Program verification II)
Slides 11b in Color (Semantics of Hoare Logic)
|
Notes on Hoare Logic (covering I and II, updated)
|
| The lambda calculus |
Slides 12 |
