Peter Baumgartner, Margret Groß-­Hardt, Alex Sinner

• The Living Book is a system for the management of personalized and scenario specific teaching material. The main goal of the system is to support the active, explorative and self­determined learning in lectures, tutorials and self study. The Living Book includes a course on 'logic for computer scientists' with a uniform access to various tools like theorem provers and an interactive tableau editor. It is routinely used within teaching undergraduate courses at our university. This paper describes the Living Book and the use of theorem proving technology as a core component in the knowledge management system (KMS) of the Living Book. The KMS provides a scenario management component where teachers may describe those parts of given documents that are relevant in order to achieve a certain learning goal. The task of the KMS is to assemble new documents from a database of elementary units called 'slices' (definitions, theorems, and so on) in a scenario-based way (like 'I want to prepare for an exam and need to learn about resolution'). The computation of such assemblies is carried out by a model-­generating theorem prover for first-­order logic with a default negation principle. Its input consists of meta data that describe the dependencies between different slices, and logic-­programming style rules that describe the scenario-specific composition of slices. Additionally, a user model is taken into account that contains information about topics and slices that are known or unknown to a student. A model computed by the system for such input then directly specifies the document to be assembled. This paper introduces the e­learning context we are faced with, motivates our choice of logic and presents the newly developed calculus used in the KMS.