Peter Baumgartner
The Slicing Books Technology (SIT) allows to structure books and other documents as small semantic units, which, depending from the user's knowledge, can be re-assembled individually in order to arrive at a document matching the user's needs.
Various tools around SIT are implemented. In the center are the authoring tool and the ``reader'' tool for the end user. Currently, we are aiming to bring in ``deduction'' into these tools. The motivation is to be able to derive accurately and on a declarative basis what units are to be re-assembled in the final document.
We will demonstrate the current state of affairs, which is a prototypical coupling of one of these tools with our FDPLL theorem prover, and report about first experiments. To be completed