This work is about a “real-world” application of automated deduction. The application is the management of documents (such as mathematical textbooks) as they occur in a readily available tool. These documents are “living”, in the sense, that they can be modified and extended by the reader, who can interact via Living Books with external systems.
A particular task is to assemble a new document from such units in a selective way, based on the user’s current interest and knowledge.
It is argued that this task can be naturally expressed through logic, and that automated deduction technology can be exploited for solving it. More precisely, we rely on first-order clausal logic with some default negation principle, and we propose a model computation theorem prover as a suitable deduction mechanism.