Tuesday, Thursday 10:00-11:20, RCH 211.
Tuesday, Thursday 1:00-2:20, MC 4020.
Tutorials.
Friday, 10:30-11:20, MC 4041.
Friday, 11:30-12:20, MC 4041.
Friday, 2:30-3:20, MC 4041.
Friday, 3:30-4:20, MC 4041.
Course work.
Assignments (25%)
Midterm exam (25%)
Final exam (50%)
Note Typesetting(5% extra credit)
Course description.
Propositional and predicate logic. Soundness and completeness
and their implications. Unprovability of formulae in certain
systems. Undecidability of problems in computation, including
the halting problem. Reasoning about programs. Correctness proofs
for both recursive and iterative program constructions.
Course 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.