Here is a list of the topics covered in each lecture, with the corresponding [H&R] book sections. We will adjust this schedule as required.

L01 | Tu Jan 8 | Notes, page 1-40 | What is logic; Logic propositions and connectives | [H&R] 1.1 | |

L02 | Th Jan 10 | Notes, page 41-49 | Truth tables; Translations from English into propositional logic; Examples and a logic puzzle | [H&R] 1.1, 1.2, 1.4.1, 1.4.2 | |

Notes, page 1-22 | Well-formed propositional logic formulas; Induction | ||||

L03 | Tu Jan 15 | Notes, page 23-38 | Proving things about logic formulas: Structural induction |
[H&R] 1.3, 1.4.2 | |

Notes, pages 1-10 | Propositional calculus, semantics: value assignments, satisfiability; a logic puzzle | [H&R] 1.4.1 | |||

L04 |
Th Jan 17 | Notes, page 11-41 | Sudoku as a satisfiability problem; Proving arguments valid in propositional logic |
[H&R] 1.5.1 | Assignment 1 posted |

L05 | Tu Jan 22 | Notes | Propositional Calculus: Formula simplification, Laws, DNF/CNF |
[H&R] 1.5.1, 1.5.2 | |

L06 | Th Jan 24 | Notes, pages 1-43 | Adequate connectives; Boolean Algebra; Logic gates; circuits |
Assignment 1 due tomorrow | |

L07 | Tu Jan 29 | Notes, pages 44-59 | Circuit minimization; Analysis and simplification of code |
||

Notes, pages 1-11 | Formal (natural) deduction |
[H&R] 1.2 (with different notation) | |||

L08 |
Th Jan 31 | Notes, pages 12-39 | Formal deduction theorems |
[H&R] 1.2, 1.4.3 (with different notation) | Assignment 2 posted |

L09 | Tu Feb. 5 | Notes, pages 40-67 | Soundness and Completeness of formal deduction |
[H&R] 1.4.4 (with different notation) | |

L10 | Th Feb. 7 | Notes | Automated theorem proving by resolution; Resolution strategies, Davis Putnam Procedure |
Assignment 2 due tomorrow | |

L11 | Tu Feb. 12 | Snow day | |
||

L12 |
Thu Feb. 14 | Notes | Predicate logic; Quantifiers |
[H&R] 2.1 | Assignment 3 posted |

Feb. 18-22 |
Reading Week |
||||

L13 | Tu Feb. 26 | Notes | Predicate logic syntax |
[H&R] 2.2 | |

Notes, pages | Predicate logic semantics |
[H&R] 2.4 (with different notation) | Assignment 3 due today | ||

L14 | Thu Feb. 28 | Notes | Logic and DNA Computing | ||

Notes | Solving Satisfiability with DNA |
||||

Midterm, 4:30-6:20 |
|||||

L15 | Tu Mar. 5 | Notes | Proving argument validity in predicate logic |
[H&R] 2.4, part of 2.5 (with different notation) | |

L16 | Th Mar. 7 | Notes, pages 1-35 | Formal (natural) deduction in predicate logic |
[H&R] 2.3 (with different notation) | |

L17 | Tu Mar. 12 | Notes, pages 36 - 42 | Formal deduction in predicate logic: Examples and exercises |
||

Notes, pages 1-13 | Resolution for predicate logic: Prenex Normal Form | ||||

L18 |
Th Mar. 14 | Notes, pages 14 - 46 | Existential-free PNF, unification and resolution, automated theorem provers |
Assignment 4 posted | |

L19 | Tu Mar. 19 | Notes | Undecidability: The Halting Problem and other undecidable problems |
[H&R] 2.5 | |

L20 | Th Mar. 21 | Notes, pages 1-21 | Peano Arithmetic |
Assignment 4 due tomorrow | |

L21 | Tu Mar. 26 | Notes, pages 22-39 | Proving theorems in Peano Arithmetic; Godel's Incompleteness Theorem |
Teaching evaluations (tentative) | |

L22 |
Th Mar. 28 | Notes, pages 1-53 | Program verification: Assignment rules, implied rules, composition rules |
[H&R] Chapter 4 (4.1, 4.2, 4.3) | Assignment 5 posted |

L23 | Tu Apr. 2 | Notes, pages 54-88 | Program verification: If-then-else rules, while rules, decidability of partial and total correctness | [H&R] Chapter 4 (4.3, 4.4) | |

L24 | Th Apr. 4 | Final Exam Review | Assignment 5 due tomorrow |