Logical Foundations of Programming, Fall 2006
Prerequisites
- college algebra
- basic imperative programming skills
Knowledge and skills that should be acquired in this course
-
Mastery
-
-
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
-
understanding what it means for a sentence to be
a consequence of other sentences
-
understanding what constitutes a logically valid argument, and
understanding the notion of a counterexample
-
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)
-
constructing proofs in the natural deduction calculus
-
converting a logic formula into equivalent
but more handy formulas (such as conjunctive normal form)
-
writing specifications (pre- and postcondition)
for simple programming problems
-
verifying the correctness of simple programs
-
Familiarity
-
-
appreciating issues that arise when attempting to translate
natural language into first-order logic
-
realizing the significance of soundness and completeness
of natural deduction for propositional logic and first-order logic
-
computing invariants for while-statements
-
being exposed to a case study of algorithm design and verification
-
seeing other kinds of
logics (such as CTL), used for the specification
of concurrent programs
Torben Amtoft