Description

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 solvers, resolution, binary decision diagrams, Post's adequacy theorem
Predicate Logic
syntax, semantics, natural deduction, undecidability, expressiveness, unification, resolution
Logic Programming
SLD resolution, Prolog, finite domain constraints
Model Checking
linear-time temporal logic, branching-time temporal logic, algorithms, fixed-point characterisation, symbolic model checking

Literature

The course is largely based on the following book:

Michael Huth and Mark Ryan
Logic in Computer Science (second edition)
Cambridge University Press, 2004
ISBN 0-521-54310-X (paperback)

Books on logic programing (week 6) and Prolog (week 7) include

Kryzstzof R. Apt
From Logic Programming to Prolog
Prentice Hall, 1997
ISBN 0-132-30368-X

William F. Clocksin and Christopher S. Mellish
Programming in Prolog (fifth edition)
Springer Verlag, 2003
ISBN 978-3-540-00678-7

Leon Sterling and Ehud Shapiro
The Art of Prolog (second edition)
MIT Press, 1994
ISBN 0-262-19338-8

Slides as well as solutions to selected exercises will be made available online.

Language

The course is taught in English. The exercises are conducted in German. Part of the contents of the course is covered in the following German book:

Uwe Schöning, Logik für Informatiker (5. Auflage), Spektrum Akademischer Verlag, 2000,
ISBN 3-8274-1005-3