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 (Introduction to Combinatorics), 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
Related courses
- Predecessors: (CS 136, 145 taken in fall 2010 or earlier or CS 146) equivalent-programming in Scheme and C; Math 135 (for 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
For official details, see the UW calendar.
Software/hardware used
Typical reference(s)
- Lu Zhongwan, 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 logics 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
- Understand the applications of logic to computer science
Typical syllabus
Introduction (1 lecture = 1.5 hours)
- History, motivation, connections to computer science
Propositional Logic (10 lectures = 15 hours)
- 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 simplification, Conjunctive/Disjunctive Normal Form.
- Adequate sets of connectives.
- Boolean algebra, logic gates, circuit design, circuit minimization.
- Formal deduction for propositional logic; proving argument validity by formal deduction (syntactically).
- Soundness and completeness of formal deduction.
- Applications of propositional logic to computer science, such as: analysis and simplifcation of code; automated proofs (resolution, Davis-Putnam procedure); hardware and software verification.
Predicate Logic (7 lectures = 10.5 hours)
- Limitations of propositional logic, and the necessity of predicate logic for reasoning about objects and properties.
- Quantifiers, universe of discourse, translation of English sentences into predicate logic formulas.
- Syntax of predicate logic, well-formed formulas.
- Semantics of predicate logic, interpretations.
- Proving argument validity in predicate logic (semantically).
- Formal deduction in predicate logic; proving argument validity by formal deduction (syntactically).
- Soundess and completeness of formal deduction for predicate logic.
- Applications of predicate logic to computer science, such as: automated theorem provers and verifiers; databases.
Decidability and Peano Arithmetic (4 lectures = 6 hours)
- The Turing Machine as a model of computation.
- Undecidability: Basic notions, undecidability of Halting Problem and other problems.
- The Peano axioms for number theory (including the induction axiom), undecidability of Peano Arithmetic.
- Godel's Incompleteness Theorem.