In the era of information technology, providing high quality and state of the art educational material is quite a challenge and requires the use of new media. The In2Math project at the University of Koblenz-Landau develops in this context the Living Book; Living Book means personalized user oriented educational material together with interactive components. The Living Book aims at supporting the fundamental parts of undergraduate classes in theoretical computer science. The main goal is to support the active, explorative and self-determined learning in lectures, tutorials and selfstudy.

This paper describes the main aspects of the Living Book and explains the concepts and ideas behind it as well as the techniques used to realized these concepts.

The Davis-Putnam-Logemann-Loveland procedure (DPLL) was introduced in the early 60s as a proof procedure for first-order logic. Nowadays, only its propositional logic core component is widely used in efficient propositional logic provers and respective applications. This success motivates to reconsider lifting DPLL to the first-order logic level in a more contemporary way, by exploiting successful first-order techniques like “unification”. Following this idea, in this paper a first-order logic version of DPLL, FDPLL, is presented.

While propositional DPLL is based on a splitting rule for case analysis wrt. ground and complementary literals, FDPLL uses a lifted splitting rule, i.e. the case analysis is made wrt. non-ground and complementary literals now. To make this work, a new way of treating variables is employed. It comes together with a compact way of representing and reasoning with first-order logic interpretations, much like propositional DPLL reasons about propositional truth assignments. As a nice consequence, FDPLL naturally decides the class of Bernays-Schönfinkel formulas, which is notoriously difficult for most other calculi.