Logical Foundations of Programming, Spring 2003

Prerequisites by topic

• college algebra
• basic imperative programming skills
• intuitive understanding of the semantics of simple imperative programs

Knowledge and skills acquired in this course

Mastery

1. understanding the syntax and semantics of first-order logic, with propositional logic as an important special case
2. understanding what it means for a sentence to be a tautology, and what it means for a sentence to be a consequence of other sentences
3. employing basic methods of proof, including proof by cases, proof by contradiction, and (not least) proof by induction
4. constructing proofs in the natural deduction calculus
5. understanding the notion of a counterexample
6. realizing the significance of soundness and completeness of natural deduction for propositional logic and first-order logic
7. verifying the correctness of simple while-programs

Familiarity

• appreciating issues that arise when attempting to translate natural language into first-order logic
• understanding what constitutes a logically valid argument
• converting a propositional logic formula into equivalent but more handy formulas (such as conjunctive normal form)
• realizing the impact of undecidability of provability/validity in first order logic
• computing invariants for while-statements
• being exposed to a case study of algorithm design and verification