Logical Foundations of Programming, Fall 2006

Prerequisites

• college algebra
• basic imperative programming skills

Knowledge and skills that should be acquired in this course

Mastery

1. understanding the syntax and semantics of first-order logic (with propositional logic as an important special case), thereby being able to translate simple English sentences into first-order logic
2. understanding what it means for a sentence to be a consequence of other sentences
3. understanding what constitutes a logically valid argument, and understanding the notion of a counterexample
4. employing basic methods of proof, including proof by cases, proof by contradiction, and proof by induction (applicable for any data structure having an inductive definition)
5. constructing proofs in the natural deduction calculus
6. converting a logic formula into equivalent but more handy formulas (such as conjunctive normal form)
7. writing specifications (pre- and postcondition) for simple programming problems
8. verifying the correctness of simple programs

Familiarity

1. appreciating issues that arise when attempting to translate natural language into first-order logic
2. realizing the significance of soundness and completeness of natural deduction for propositional logic and first-order logic
3. computing invariants for while-statements
4. being exposed to a case study of algorithm design and verification
5. seeing other kinds of logics (such as CTL), used for the specification of concurrent programs