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 
lineartime temporal logic, branchingtime temporal logic, algorithms, fixedpoint 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 052154310X (paperback)

Kryzstzof R. Apt
From Logic Programming to Prolog
Prentice Hall, 1997
ISBN 013230368X

William F. Clocksin and Christopher S. Mellish
Programming in Prolog (fifth edition)
Springer Verlag, 2003
ISBN 9783540006787

Leon Sterling and Ehud Shapiro
The Art of Prolog (second edition)
MIT Press, 1994
ISBN 0262193388
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 3827410053