en | de


bachelor program

VO3 + PS2  WS 2008/2009  703019 + 703020


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


The course is largely based on the following book: Books on logic programing (week 6) and Prolog (week 7) include Slides as well as solutions to selected exercises will be made available online.


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: