|
|
Syllabus
I. Introduction
Lectures: ~1
|
What is logic?
Informal and formal logical reasoning
Motivation
|
II. Propositional Logic
Lectures: ~6
|
Syntax of formulas
Formalizing English sentences
Semantics
Transformational proofs (Laws)
Hilbert Style proofs (Laws)
Natural deduction proofs(Laws)
Natural deduction proof Strategies(Strategies)
Semantic tableaux proofs
Soundness and completeness
Finding counterexamples
Induction
Applications
|
III. Predicate Logic
Lectures: ~8
|
Syntax of formulas
Formalizing English sentences
Semantics
Transformational proofs
Natural deduction proofs
Semantic tableaux proofs
Soundness and completeness
Finding counterexamples
Induction
Applications
|
IV. Sets, Relations, Functions
Lectures: ~2
|
Formalization
Proofs and proof strategies
|
V. Decidability and Program Verification
Lectures: ~8
|
Undecidability, the halting problem and reductions
Partial and total correctness
Proving functional programs correct
Proving imperative programs correct:
pre-conditions, post-conditions, and loop invariants;
proof rules; handling conditionals, for loops,
and while loops
|
|