Revised Feb. 10, 2014
CS 245: Logic and Computation
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 knowledge of propositional and predicate logic, including key notions, such as the distinction between syntax and semantics and between "provable" and "valid"
- Explore the limits of computers, including computability and non-computabilty
- Use logical skills to reason about computer programs
- 2A students in Computer Science and Computational Mathematics
For official details, see the UW calendar.
- 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 CS 360/365 (and then most CS upper-year courses)
- Co-requisites: None
- Conflicts: PMATH 330; SE 112/212
- Lu Zhangwan, Mathematical Logic for Computer Science, 2nd ed., World Scientific
At the start of the course, students should be able to
- Code in at least two programming languages, ideally one functional (e.g., Scheme) and one imperative (e.g. C or C++), such as provided by CS 135 and CS 136
- Work with proofs in discrete mathematics, such as those encountered in Math 135
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 to interpret such formulae in English
- Prove the correctness (or incorrectness) of simple formulae in the propositional and predicate logic by natural deduction (or by counterexample) and find errors in purported proofs
- Describe transformational (algebraic) proof for proving statements in the propositional and predicate logic
- Explain the concepts of partial decidability and of undecidability giving examples of each; apply reductions to demonstrate certain problems have these difficulties
- Annotate short programs with loop or recursive invariants to aid in debugging and proving assertions about simple programs
- Prove the correctness of simple programs in a functional language and in a basic subset of an imperative language
Introduction (1) hours
Propositional Logic (13) hours
- Informal and formal logical reasoning
- Formal proof systems and semantics
Predicate Logic (10) hours
- 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.
Decidability and Program Verification (12) hours
- 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.
Last modified: Friday, 06-Jun-2014 15:16:48 EDT