In this course, it will be shown, how to express real-world facts and their relationships in logic and how to transform a corresponding specification into an executable Prolog program. Moreover, the features of the logic programming language Prolog will be explained, including rules, unification, SLD-resolution, and backtracking. Additionally, the logic database query language Datalog will be discussed and it will be shown how to infer information from a deductive database. Also, the use of constraint solving from Prolog will be treated.

Business rules management systems such as Drools enable the expression of volatile business logic and their integration into an information system. Such systems and the way they evaluate rules will be presented.

Finally, it will be taught, how to express temporal relationships by temporal logics such as CTL and LTL. Then, it will be shown, how to automatically check information systems for compliance with a temporal specification by using a model checker.