Assignments are due at 11:00am (Waterloo time) on due dates.
Acknowledgement: The lecture materials contain content created by Shai Ben-David, Jonathan Buss, Alice Gao, Lila Kari, Anna Lubiw, Prabhakar Ragde, Collin Roberts, Richard Trefler, et al. for previous iterations of the course.
Date | Lectures & Tutorials | Notes & Readings | Assignments & Exams |
---|---|---|---|
May 3 | What is logic? Logic propositions and connectives. |
Logic 01
Lu 2.1 Z1 |
|
May 5 | Truth tables; translations between English and propositional logic; propositional logic formulas; review of induction. |
Logic 02
Lu 1.2, 2.2 Z2 |
|
May 6 | No tutorial |
T1
|
|
May 10 | Structural induction; propositional language semantics; satisfiability. |
Logic 03
Lu 2.3, 2.4 Z3 |
|
May 12 | Tautological consequence; proving arguments valid in propositional logic. |
Logic 03
Lu 2.5 Z4 |
Assignment 1 available |
May 13 | Tutorial |
T2
|
|
May 17 | Propositional calculus laws; disjunctive and conjunctive normal forms. |
Logic 04
Lu 2.7 Z5 |
Assignment 1 due May 18 |
May 19 | Adequate set of connectives; Boolean algebra; logic gates. |
Logic 05
Lu 2.8 Z6 |
|
May 20 | Tutorial |
T3
|
|
May 24 | Circuit design and minimization; code analysis and simplification. |
Logic 05
Z7 |
|
May 26 | Formal deduction for propositional logic. |
Logic 06
Lu 2.6 Z8 |
Assignment 2 available |
May 27 | Tutorial |
T4
|
|
May 31 | Soundness and completeness of formal deduction for propositional logic (proof of completeness optional). |
Logic 06
Lu 2.6 Z9 |
Assignment 2 due June 1 |
June 2 | Automated theorem proving: resolution, Davis-Putnam procedure (proof of completeness of DPP optional). |
Logic 07
Z10 |
|
June 3 | Tutorial |
T5
|
|
June 7 | First-order logic: domain, terms, relations, variables, quantifiers; translations from English to first-order logic. |
Logic 10
Lu 3.1 Z11 |
|
June 9 | Midterm review. | Midterm, June 9 | |
June 10 | No tutorial |
T6
|
|
June 14 | First-order logic syntax and semantics. |
Logic 11
Logic 12 Lu 3.2, 3.3 Z13 |
|
June 16 | Logical consequence in first-order logic. |
Logic 13
Lu 3.4 Z14 |
Assignment 3 available |
June 17 | Tutorial |
T7
|
|
June 21 | Formal deduction in first-order logic. |
Logic 14
Lu 3.5 R15 Z15 |
Assignment 3 due June 22 |
June 23 | Formal deduction in first-order logic: more proof examples, soundness and completeness. |
Logic 14
Lu 3.5 R16 Z16 |
|
June 24 | Tutorial |
T8
|
|
June 28 | Resolution for first-order logic: prenex normal form, existential-free PNF, unification and resolution. |
Logic 15
Lu 3.6 R17 Z17 |
|
June 30 | Resolution for first-order logic: proof examples. Computation and logic: the satisfiability problem, the halting problem. |
Logic 15
Logic 16 R18 Z18 |
Assignment 4 available |
July 1 | No tutorial (Canada Day) |
T9
|
|
July 5 | Turing machines; computability and decidability. |
Logic 16
R19 Z19 |
Assignment 4 due July 6 |
July 7 | Proving decision problems undecidable by reduction. |
Logic 16
Z20 |
|
July 8 | Tutorial |
T10
|
|
July 12 | Peano arithmetic. |
Logic 17
R21 Z21 |
|
July 14 | Proving theorems in Peano arithmetic; Gödel's incompleteness theorem. |
Logic 17
R22 Z22 |
Assignment 5 available |
July 15 | Tutorial |
T11
|
|
July 19 | Program verification: Hoare triples, partial and total correctness, rules for assignment, implication, and composition. |
Logic 20
Z23 |
|
July 21 | Program verification: conditional statements, partial-while, program termination, undecidability of partial and total correctness. Course review. |
Logic 20
Z24 |
|
July 22 | Tutorial |
T12
|
|
July 26 | No lecture (July 26 follows a Friday schedule) | Assignment 5 due July 26 | |
Aug 2 | Exam Week | ||
Aug 9 | Exam Week | Final exam, August 9 |