CS 245E: Logic and Computation, Enriched (Fall 2026)

General Information

Course Description

CS 245E is the enriched version of CS 245. It develops the mathematical and computational logic background required in the Computer Science program. The core of the course covers propositional and first-order logic, formal deduction, computability and program verification.

For the Fall 2026 CS245E offering, the regular CS245 material is covered more rapidly or in more depth and enrichment topics are given to connect with applications and related areas.

Objectives

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

formalize English sentences as formulas in propositional and first-order logic, and interpret such formulas in English;
understand syntax, semantics, consequence, formal proof, soundness, and completeness;
construct and check formal proofs and understand the difference between finding a proof and checking a proof;
use normal forms, adequate connectives, Boolean algebra, and resolution in computational settings;
understand how logic is used in circuits, proof assistants, SAT/SMT solvers, and program verification;
explain the roles of Peano arithmetic, Turing machines, reductions, undecidability, and Gödel incompleteness;
use software tools for proof verification.

Overview

The course is organized into five connected blocks. The enriched material is intended to show how syntax, semantics, proof, computation, decidable fragments, and verification fit together.

Propositional Logic and Finite-State Systems

Landscape of logics; propositional syntax and semantics; structural induction; adequate connectives.
Algebraic structures, Boolean algebra, combinational circuits, normal forms, formula minimization, memory, finite-state machines, and temporal logic.

Formal Propositional Proof and Automating Tools

Formal deduction, proof checking, soundness and completeness.
Resolution, SAT, and the first software tools: Logicat and Lean.

Formal First-Order Proof and Automating Tools

Quantifiers, first-order syntax, semantics, consequence, validity, formal deduction, soundness and completeness.
Unification, SMT, Horn clauses, Prolog, and Z3.

Axiomatic Theories, Computability, and Decidability

Axiomatic theories and models, group theory as an example, Peano arithmetic and arithmetic truth.
Turing machines, encodings, computability, reductions, undecidability, Gödel incompleteness, Presburger arithmetic and decidable arithmetic.

Program Specification and Verification

Specifications, Hoare triples, assignments, conditionals, loops, arrays, functions, and recursion.
Connections to SMT: Presburger arithmetic for indices and bounds, array theory for array contents, and logical verification conditions for programs.

Course Meet Times

Lectures meet Tuesdays and Thursdays for 80 minutes with tutorial sessions on Fridays. Students should consult Quest for lecture, tutorial, and room information.

Schedule

This schedule is provisional and will be updated by September 17 and will be adjusted during the term as required. Tutorials provide practice with the preceding lecture material and software tools. Assignments are cumulative unless explicitly stated otherwise.

Midterm: The Midterm Exam will be Thu Oct 29. It will cover all material through the end of Week 6, including LE11.

Final: There will be a Final Exam during the university's final exam period. It will cover the entire course.

Week	Lectures		Tutorials	Assessments
Week	Tuesday	Thursday	Friday	Assessments
#1: 09/10–09/13		LE01 The Landscape of Logics, start of LE02	No tutorial
#2: 09/14–09/20	LE02 Propositional Logic Syntax, Structural Induction, Adequate Connectives	LE03 Propositional Logic Semantics, Proving Propositional Arguments Valid	Logicat, semantic consequence	Assignment 1 released Wed Sep 16
#3: 09/21–09/27	LE04 Algebraic Structures and Combinational Circuits	LE05 Normal Forms, Minimization of Logical Formulas	Worked problems
#4: 09/28–10/04	LE06 Flip-Flops, Memory, Finite State Machines	LE07 Temporal Logic	Worked problems	Assignment 1 due Mon Sep 28 Assignment 2 released Wed Sep 30
#5: 10/05–10/09	LE08 Formal Deduction for Propositional Logic	LE09 Soundness and Completeness, LEAN	LEAN: proof terms and checking formal proofs
10/10–10/18	Reading Week. No classes, tutorials or regular office hours.
#6: 10/19–10/25	LE10 Resolution Proving, SAT	LE11 Quantifiers, First-Order Logic Syntax	Worked problems	Assignment 2 due Mon Oct 19 Assignment 3 released Wed Oct 21
#7: 10/26–11/01	LE12 First-Order Semantics	Midterm / study-exam slot	Worked problems	Midterm Exam: Thu Oct 29
#8: 11/02–11/08	LE13 First-Order Consequence and Proving First-Order Arguments Valid	LE14 First-Order Formal Deduction	Worked problems	Assignment 3 due Mon Nov 2 Assignment 4 released Wed Nov 4
#9: 11/09–11/15	LE15 Unification, SMT, Horn Clauses and Prolog	LE16 Axiomatic Theories (e.g. Group Theory), Peano Arithmetic	Z3: SMT with equality and arithmetic examples
#10: 11/16–11/22	LE17 Turing Machines, Computability, Reductions	LE18 Undecidability, Gödel Incompleteness	Worked problems	Assignment 4 due Mon Nov 16 Assignment 5 released Wed Nov 18
#11: 11/23–11/29	LE19 Presburger Arithmetic and Decidable Arithmetic	LE20 Program Specification, Hoare Triples, Program Verification	Worked problems
#12: 11/30–12/06	LE21 Assignments, Conditionals, Loops	LE22 Arrays, Functions, Recursion	Worked problems
#13: 12/07–12/08	LE23 Review		No tutorial	Assignment 5 due Mon Dec 7

Office Hours

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. For administrative questions, contact the coordinator, Dalibor Dvorski, by email: ddvorski@uwaterloo.ca .

Instructor

Stephen Watt: Tuesdays and Thursdays 1:10 to 2:15 in DC 3621

Teaching Assistants

Nosa Efemwonkieke, Alena Gusakov, Ende Jin, Farnam Mansouri

Grading Scheme

Assignments: 30%
Midterm Exam: 30%
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 or other AI chatbots 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
students will not be exempted from more than two assignments for any reason.

Assignments

There will be five assignments. Each assignment will be released on a Wednesday. The first four assignments are due on the Monday before the next assignment is released; Assignment 5 is due on Monday, December 7.

Assignment 1: released September 16; due September 28.
Assignment 2: released September 30; due October 19.
Assignment 3: released October 21; due November 2.
Assignment 4: released November 4; due November 16.
Assignment 5: released November 18; due December 7.

Late Submission of Assignments

Here are the details about how late 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.

Textbook

The recommended textbook for the standard CS245 course has been 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.

The enriched course will have details of additional reference material in the lecture slides. Lecture slides for the course will be available electronically on LEARN .

Piazza — Discussion Forum Guidelines

Please search Piazza to see whether your question has already been answered to avoid posting a duplicate question. This should benefit everyone in three 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.
- Students will have less to read to keep up with the forum.
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.