CS 245: Logic and Computation (Fall 2023)

General Information

Course Description

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:

develop mathematical reasoning skills;
improve understanding of propositional and first-order logic, including key notions, such as: expressing natural language statements as logical formulas, distinguishing between correct and incorrect reasoning (between valid and invalid logical arguments), constructing a formal proof, distinguishing between syntax and semantics; and
explore the limits of computers, including computability and uncomputability.

Objectives

At the end of the course, students should be able to:

formalize English sentences into properly formed formulas in the propositional and first-order logic and, conversely, interpret such formulas in English;
formalize the notion of correct reasoning and proof, and be able to construct formal proofs;
realize the limitation of formal proof systems; and
understand the applications of logic to computer science

Overview

introduction: history, motivation, connections to computer science
propositional logic:
- connectives, truth tables, translation of English sentences into propositional logic
- syntax: well-formed-formulas in propositional logic; structural induction and its use in proving statements about logic formulas
- semantics: value assignments, how to (semantically) prove that arguments in propositional logic are valid (i.e., correct, sound)
- essential laws for propositional logic, formula simpliﬁcation, Conjunctive/Disjunctive Normal Forms
- adequate sets of connectives
- Boolean algebra, logic gates, circuit design, circuit minimization
- formal deduction for propositional logic; proving arguments valid by formal deduction (syntactically)
- soundness and completeness of formal deduction
- applications of propositional logic to computer science, such as: analysis and simpliﬁcation of code; automated proofs: resolution, Davis-Putnam Procedure; hardware and software veriﬁcation
first-order logic:
- limitations of propositional logic, and the necessity of first-order logic for reasoning about objects and properties
- quantiﬁers, universe of discourse, translation of English sentences into first-order logic formulas
- syntax of first-order logic, well-formed formulas
- semantics of first-order logic, interpretations
- proving argument validity in first-order logic (semantically)
- formal deduction in first-order logic; proving argument validity by formal deduction (syntactically)
- applications of first-order logic to computer science, such as: Automated theorem provers and veriﬁers; databases
decidability and Peano arithmetic:
- Turing machine as a model of computation
- undecidability: basic notions, undecidability of the halting problem and other problems
- the Peano axioms for number theory (including the induction axiom), undecidability of Peano arithmetic
- Godel's incompleteness theorem
an important application of logic to computer science:
- program verification:
  - Hoare triples
  - inference rules for assignments, conditionals, while-loops
  - partial and total completeness
review for midterm and final exams (optional)

Course Meet Times

Lectures

Section	Time	Location	Instructor
LEC 001	Tuesdays and Thursdays, 8:30 – 9:50 a.m.	MC 1056	Stephen Watt
LEC 002	Tuesdays and Thursdays, 10:00 – 11:20 a.m.	MC 1056	Stephen Watt
LEC 003	Tuesdays and Thursdays, 11:30 a.m. – 12:50 p.m.	MC 1056	Lila Kari
LEC 004	Tuesdays and Thursdays, 1:00 – 2:20 p.m.	MC 4045	Collin Roberts
LEC 005	Tuesdays and Thursdays, 2:30 – 3:50 p.m.	MC 2017	Lila Kari

Tutorials

Section	Time	Location	Instructional Apprentice
TUT 101	Fridays, 9:30 – 10:20 a.m.	MC 4042	Fatemeh Alipour
TUT 102	Fridays, 10:30 – 11:20 a.m.	MC 4042	Fatemeh Alipour
TUT 103	Fridays, 11:30 a.m. – 12:20 p.m.	MC 4042	Ru Ji
TUT 104	Fridays, 12:30 – 1:20 p.m.	MC 4042	Jianlin Li
TUT 105	Fridays, 1:30 – 2:20 p.m.	MC 4042	Jianlin Li
TUT 106	Fridays, 11:30 a.m. – 12:20 p.m.	MC 4060	Monireh Safari
TUT 107	Fridays, 12:30 – 1:20 p.m.	MC 4060	Monireh Safari

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.

Schedule

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
Week	Tuesday	Thursday	Friday	Assessments	References
#1: 09/04–09/08		What is logic? Logic propositions and connectives.	No tutorial on 09/08; notes provided.	Marked Quiz 1 released on 09/08	Logic01 [Lu] 2.1
#2: 09/11–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.	Marked Quiz 1 due 09/13, 11:59 PM Crowdmark Assignment 1 released by 09/13	Logic02 Logic03 (#1–19) [Lu] 1.2–2.4
#3: 09/18–09/22	Proving arguments valid in propositional logic.	Propositional calculus laws; Disjunctive and Conjunctive Normal Forms.	Argument validity; Disjunctive and Conjunctive Normal Forms.	Crowdmark Assignment 1 due 09/20, 11:59 PM Marked Quiz 2 released by 09/20	Logic03 (#20–end) Logic04 [Lu] 2.5, 2.7
#4: 09/25–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.	Marked Quiz 2 due 09/27, 11:59 PM Crowdmark Assignment 2 released by 09/27	Logic05 [Lu] 2.8
#5: 10/02–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.	Crowdmark Assignment 2 due 10/04, 11:59 PM Marked Quiz 3 released by 10/04	Logic06 [Lu] 2.6
10/09–10/13	Reading Week. No classes, office hours or tutorials.
#6: 10/16–10/20	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.	Marked Quiz 3 due 10/18, 11:59 PM Crowdmark Assignment 3 released by 10/18	Logic07 Logic10 [Lu] 3.1 [Lu] 3.2
#7: 10/23–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/25, 11:59 PM	Logic11 Logic12 Logic13 [Lu] 3.2 [Lu] 3.3 [Lu] 3.4
#8: 10/30–11/03	Formal deduction in first–order logic.	Self-study (classes cancelled)	No tutorial on 11/03; notes provided for formal deduction in first–order logic.	Midterm Exam: 11/02, 4:30–6:20 p.m. Marked Quiz 4 released by 11/01	Logic14 [Lu] 3.5
#9: 11/06–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.	Marked Quiz 4 due 11/08, 11:59 PM Crowdmark Assignment 4 released by 11/08	Logic14 Logic15 [Lu] 3.5, 3.6
#10: 11/13–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.	Crowdmark Assignment 4 due 11/15, 11:59 PM Marked Quiz 5 released by 11/15	Logic16a Logic16b
#11: 11/20–11/24	Peano arithmetic.	Proving theorems in Peano arithmetic; Godel's incompleteness theorem.	Peano arithmetic; Godel's incompleteness theorem.	Marked Quiz 5 due 11/22, 11:59 PM Crowdmark Assignment 5 released by 11/22	Logic17
#12: 11/27–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 on the week of 11/27–12/01.	Logic18
#13: 12/04–12/05	Program Verification: partial-while; Program termination; Undecidability of Partial and Total Correctness; Course Review.			Crowdmark Assignment 5 due 12/05, 11:59 PM	Logic18

Office Hours

For questions concerning course material, please join us during our scheduled office hours. 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.

Instructors

Lila Kari: Tuesdays and Thursdays, 13:00–14:00 (on campus: DC 3132)
Collin Roberts: Wednesdays (up to December 6), 13:00–15:00, December 7, 14:00–15:00, December 8, 14:00–16:00, or by appointment (on campus: DC 3108, online: Microsoft Teams)
Stephen Watt: Thursdays (on campus: DC 3621) and Fridays (online: Microsoft Teams), 11:45–12:45

Instructional Apprentices

Ru Ji: Mondays, 8:30–11:30 (online: Microsoft Teams)
Fatemeh Alipour: Mondays, 13:00–15:00 (online: Microsoft Teams)
Jianlin Li: Fridays, 8:30–9:30 and 14:30–15:30 (online: Microsoft Teams)
Monireh Safari: Thursdays, 16:00–18:00 (online: Microsoft Teams)

Grading Scheme

Marked Quizzes: 10%
Crowdmark Assignments: 25%
Midterm Exam: 25%
Final Exam: 40%

Notes:

students must pass the weighted exam portion of the course (Midterm Exam, Final Exam) in order to pass the course
the work you submit must be your own (e.g., the use of ChatGPT is not permitted), and written in your own words, with references to any sources that you have used; you may discuss the assignment questions verbally with others but should come away from these discussions with no electronic or written records

Textbook

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.

Late Submission of Crowdmark Assignments

Here are the details about how late Crowdmark assignments will be handled:
- For full credit, you must submit your solutions by the specified due date and time.
- A 3% late penalty will be applied for each hour that you are late in submitting.
- If you have submitted anything before the deadline, then Crowdmark will not let you re-submit after the deadline passes. This means that you must decide whether to exercise your option to submit late before the deadline, and refrain from making a partial submission in this case.

Practice Quizzes

Here are the details about how the practice quizzes will work:
- There will be at least one practice quiz per week.
- The purpose of the practice quizzes is to give you more frequent practice with the course material than the Crowdmark assignments will.
- Each practice quiz will be automatically graded once you submit it, so that you will have immediate feedback about how you did.
- You may take each practice quiz as many times as you like.

Marked Quizzes

Here are the details about how the marked quizzes will work:
- There will be a marked quiz due in each week when there will not be a Crowdmark assignment due or a mid-term examination. The due dates for the marked quizzes are displayed on the course schedule page.
- No late submissions of marked quizzes will be accepted.
- From the time you start taking the marked quiz, you will have one hour in which to complete it. You must submit your quiz before this hour elapses and before the due date and time to receive credit.
- You will have a maximum of two attempts at each marked quiz. If you make two attempts, then the higher grade will count.
- Your grading for each marked quiz will be displayed on LEARN after the due date and time has passed.
- Your marked quiz will be randomly customized for you. We will ensure that the variations of any given question are all of the same difficulty.

Piazza Guidelines

Please search Piazza to see whether your question has already been answered, before posting a duplicate question. This should benefit us all in two obvious ways:
- You may find that your answer is already posted. In this case you will not need to wait for someone to respond.
- The overall volume of posts will be minimized, allowing the course staff to respond more quickly to all of the questions.
The instructors also wish to take this opportunity to remind the class of our general expectations about how you will use the Piazza platform.
- In accordance with university policies, please always be respectful and professional when posting to our course Piazza site.
- If you need to give feedback about an aspect of the course which you do not like, then please do so in a constructive manner.