CS 245 plays a key role in the development of mathematical skills required in the Computer Science program, and thus complements MATH 135 (Algebra), MATH 239 (Graph Theory and Enumeration), and STAT 230 (Probability). The course covers a variety of topics related to "logic and computation" that are required as background for other courses in Computer Science. It differs both in tone and content from a "logic" course one would typically find in a mathematics program. The course aims to:
At the end of the course, students should be able to:
Students may view their lecture and tutorial times and locations on
Quest.
For more information, see: How do I view my class schedule?.
If you wish to register or to change sections, either use Quest or contact a Computer Science academic advisor. The instructors and course coordinator do not support course registrations.
We will adjust this schedule as required.
Each tutorial will provide a forum for you to practice with the ideas and techniques presented in the preceding lectures. The following assignment allows further practice and feedback. Each assignment will focus on the recent topics, but includes everything that came before, as well — everything is cumulative.
The Midterm Exam will cover the material up to the end of Week #7.
There will be a Final Exam during the university's final exam period, which will cover the entire course.
| Week | Lectures | Tutorials | Assessments | References | ||
|---|---|---|---|---|---|---|
| Tuesday | Thursday | Friday | ||||
| #1: 09/04–09/08 |
What is logic? Logic propositions and connectives. |
No tutorial on 09/06; notes provided. | Marked Quiz 1 released on 09/06 |
|
||
| #2: 09/09–09/15 |
Truth tables; translations between English and propositional logic; propositional logic formulas; review of induction. | Structural induction; propositional language semantics; satisfiability. | Structural induction. Semantics of propositional logic. |
|
|
|
| #3: 09/16–09/22 |
Proving arguments valid in propositional logic. | Propositional calculus laws; Disjunctive and Conjunctive Normal Forms. | Argument validity; Disjunctive and Conjunctive Normal Forms. |
|
|
|
| #4: 09/23–09/29 |
Adequate set of connectives; Boolean algebra; logic gates. | Circuit design and minimization; code analysis and simplification. | Adequate sets of connectives, circuit design, code analysis and simplification. |
|
|
|
| #5: 09/30–10/06 |
Formal deduction for propositional logic. | Soundness and completeness of formal deduction for propositional logic (proof of completeness optional). | Formal deduction for propositional logic; soundness and completeness of formal deduction. |
|
|
|
| #6: 10/07–10/11 |
Automated theorem-proving: resolution, Davis-Putnam Procedure (proof of soundess and completeness of DPP, starting at slide 35 of Logic07: optional). | First-order logic: domain, terms, relations, variables, quantifiers. Translations from English to first-order logic. |
Resolution for propositional logic, DPP, Introduction to first-order logic. |
|
|
|
| 10/12–10/20 | Reading Week. No classes, office hours or tutorials. |
|||||
| #7: 10/21–10/27 |
First–order logic syntax and semantics. | Logical consequence in first–order logic. | First–order logic: syntax, semantics; Logical consequence in first–order logic. | Crowdmark Assignment 3 due 10/23, 11:59 PM |
|
|
| #8: 10/28–11/03 |
Self-study (classes cancelled) | Formal deduction in first–order logic. | Formal deduction in first–order logic. |
|
|
|
| #9: 11/04–11/10 |
Formal deduction in first–order logic: proof examples. | Resolution for first–order logic: Prenex Normal Form, Existential-free PNF, unification and resolution, automated theorem provers/verifiers. | Formal deduction in first–order logic; resolution for first–order logic. |
|
|
|
| #10: 11/11–11/17 |
Computation and logic: Turing machines, undecidability, the halting problem. | Turing machine examples, the undecidable tiling problem (optional), decidability and complexity of some logic problems. | Decidability; undecidability. |
|
|
|
| #11: 11/18–11/24 |
Peano arithmetic. | Proving theorems in Peano arithmetic; Godel's incompleteness theorem. | Peano arithmetic; Godel's incompleteness theorem. |
|
Logic17 | |
| #12: 11/25–12/01 |
Program verification: Hoare triples, partial and total correctness, rules for assignment, implication, composition. | Program verification: conditional statements. | Program verification: assignment, implication, composition, conditional statements. | No assessments. | Logic18 | |
| #13: 12/02–12/03 |
Program Verification: partial-while; Program termination; Undecidability of Partial and Total Correctness; Course Review. | Crowdmark Assignment 5 due 12/03, 11:59 PM | Logic18 | |||
For questions concerning course material, please join us during our scheduled office hours. Note that office hours will start at the second week of the term, and that we will not hold office hours during the Reading Week break. Times listed below are in Eastern Time. Note whether specific office hours are on campus or online; and refer to LEARN on how to connect to online office hours. If the below times do not suit you, contact an instructor to schedule an meeting. For administrative questions, contact the coordinator, Dalibor Dvorski, by email: ddvorski@uwaterloo.ca.
Notes:
The recommended textbook for this course is Mathematical Logic for Computer Science, second edition, by Lu Zhongwan. Students may access an electronic version of the textbook through the library. Please note that this book does not cover all the material presented in the course, and is meant mainly for definitions, notation, and the sections on formal deduction. For the rest of the material, students should take notes from the course and work from these. Lecture slides for the course are available electronically on LEARN.