'Living Book': -'Deduction', 'Slicing', 'Interaction'

摘要

This system description is about a real-world application of automated deduction. The system that we describe-The Living Book-is a tool for the management of personalized teaching material. The main goal of the Living Book system is to support the active, explorative and self-determined learning in lectures, tutorials and self study. It includes a course on 'logic for computer scientists' with a uniform access to various tools like theorem provers and an interactive tableau editor. This course is routinely used within teaching undergraduate courses at our university.