Revised April 28, 2010
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). It covers a variety of topics
related to "logic and computation" that are required as background for
other courses in Computer Sciece. It differs both in tone and content
from a "logic" course one would typically find in a mathematics
program. More specifically, the course has the following goals.
- To continue the students' development of skills in discrete mathematics.
-
To gain a facility with propositional and predicate logic,
including key notions such as the distinction between syntax and
semantics and between "provable" and "valid".
-
To explore the limits of computers: computability and non-computabilty.
-
To use logical skills to reason about computer programs.
Logistics
Intended for 2A students in Computer Science and Computational
Mathematics. Normally available Fall, Winter and Spring.
Related courses (see calendar for official details)
- 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. Through these, most CS upper-year courses.
-
Conflicts: PMATH 330; SE 112/212.
Typical Reference(s) 2ED
Lu Zhangwan, Mathematical Logic for Computer Science, 2nd ed.,
World Scientific.
Required preparation
- Experience in programming 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.
-
Experience with proofs in discrete mathematics, such as those
encountered in Math 135.
Learning objectives
By the end of the course, students should have the ability 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.
-
Demonstrate a basic understanding of 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.
Typical syllabus
Introduction (1 hr)
Motivation. Informal and formal logical reasoning. Formal proof
systems and semantics.
Propositional Logic (13 hrs)
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.
Predicate Logic (10 hrs)
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.
Decidability and Program Verification (12 hrs)
Undecidability of several computational issues, including halting.
Proofs of correctness of programs: a formal treatment of functional
programs and a less formal treatment of imperative programs.
The notions of partial and total correctnesss.
Undecidability, the halting problem and several reductions (using
Scheme as the model of computation).
Proving functional programs correct by induction on the length of the
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: Wednesday, 15-Feb-2012 10:31:57 EST
