Revised August 12, 2022
CS 245: Logic and Computation
General 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 discrete mathematics skills
- Improve understanding of propositional and predicate 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
- Explore the limits of computers, including computability and non-computabilty
Logistics
Audience
- 2A students in Computer Science
Normally available
- Fall, Winter, and Spring
Related courses
- Predecessors: (CS 136, 145 taken in fall 2010 or earlier or CS 146) equivalent-programming in Scheme and C; Math 135-proofs and rigour
- Successors: CS 240 and most CS uppder year courses such as CS 348, CS 360/365, CS 448, CS 486
- Co-requisites: None
- Conflicts: PMATH 330; SE 112/212
Software/hardware used
- Not applicable.
Typical reference(s)
- Lu Zhangwan, Mathematical Logic for Computer Science, 2nd ed., World Scientific
Required preparation
At the start of the course, students should be able to- Work with proofs in discrete mathematics, such as those encountered in Math 135
Learning objectives
At the end of the course, students should be able to- Formalize English sentences into properly formed formulae in the propositional and predicate logic, and conversely, interpret such formulae in English
- Formalize the notion of correct reasoning and proof, and be able to construct formal proofs.
- Realize the limitation of formal proof systems
- Prove the corr
Typical syllabus
Introduction (1 hour)- Motivation
- Informal and formal logical reasoning
- Formal proof systems and semantics
- The syntax of formulas. Review of proofs by structural induction; its use to prove formulas well-formed. Formal proof systems for the propositional calculus; the rules of natural deduction for propositional logic, including some derived rules (e.g., proof by contradiction, law of the excluded middle).
- Semantic interpretation of formulas (truth tables, Boolean algebra).
- Translation between English sentences and propositional formulas; discrepancies between the two (e.g., propositional arrow vs. causal implication).
- Soundness and completeness; Application: semantic demonstration of non-provability, consistency and satisfiability.
- The distinction between objects and properties; syntax of formulas. Formalizing English sentences.
- Additional rules of natural deduction for predicate logic (including equality). Semantic interpretation of formulas (model theory).
- Soundness and completeness and their implications.
- Demonstrating nonprovability of formulas by constructing models which provide counterexamples.
- Consistency, satisfiability, and compactness. Applying compactness to demonstrate the limits of expressibility.
- Undecidability of several computational issues, including halting. Proofs of correctness of functional and imperative programs.
- The notions of partial and total correctnesss.
- Undecidability, the halting problem, and several reductions (using Scheme as the model of computation).
- Annotating imperative programs with pre-conditions, post-conditions, and loop invariants. Proving correctness of loops by induction on the number of iterations.
