Content

The course provides an introduction to logic and model checking. The following topics are discussed:

• propositional logic: syntax, semantics, natural deduction, soundness and completeness, conjunctive normal forms, Horn clauses, SAT solving, resolution, binary decision diagrams, Post's adequacy theorem, sorting networks
• predicate logic: syntax, semantics, natural deduction, undecidability, first-order theories, Gödel's incompleteness theorem, compactness, expressiveness, unification, resolution, Skolemization
• model checking: linear-time temporal logic, branching-time temporal logic, algorithms, fixed-point characterisation, symbolic model checking