Logic for CS


Lecture 1 - Introduction


Lecture 2 - Propositional Logic Syntax


Lecture 3 - Semantics of Propositional Logic


Lecture 4 - Logical and Algebraic Concepts


Lecture 5 - Identities and Normal forms


Lecture 6 - Tautology Checking


Lecture 7 - Propositional Unsatisfiability


Lecture 8 - Analytic Tableaux


Lecture 9 - Consistency and Completeness


Lecture 10 - The Completeness Theorem


Lecture 11 - Maximally Consistent Sets


Lecture 12 - Formal Theories


Lecture 13 - Proof Theory : Hilbert-style


Lecture 14 - Derived Rules


Lecture 15 - The Hilbert System : Soundness


Lecture 16 - The Hilbert System : Completeness


Lecture 17 - Introduction to Predicate Logic


Lecture 18 - The Semantic of Predicate Logic


Lecture 19 - Subsitutions


Lecture 20 - Models


Lecture 21 - Structures and Substructures


Lecture 22 - First-Order Theories


Lecture 23 - Predicate Logic: Proof Theory (Continued...)


Lecture 24 - Existential Quantification


Lecture 25 - Normal Forms


Lecture 26 - Skalemization


Lecture 27 - Substitutions and Instantiations


Lecture 28 - Unification


Lecture 29 - Resolution in FOL


Lecture 30 - More on Resolution in FOL


Lecture 31 - Resolution : Soundness and Completeness


Lecture 32 - Resolution and Tableaux


Lecture 33 - Completeness of Tableaux Method


Lecture 34 - Completeness of the Hilbert System


Lecture 35 - First-Order Theories


Lecture 36 - Towards Logic Programming


Lecture 37 - Verification of Imperative Programs


Lecture 38 - Verification of WHILE Programs


Lecture 39 - References