Three real world applications are depicted which all have in common, that their core component is a full first order theorem prover, based on the hyper tableau calculus. These applications concern information retrieval in electronic publishing, the integration of description logics with other knowledge representation techniques and XML query processing.

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 editorThis work is sponsored by EU IST-Grant TRIAL-SOLUTION and Bmbf-Grant In2Math.. This course is routinely used within teaching undergraduate courses at our university.

The DPLL procedure, due to Davis, Putnam, Logemann, and Loveland, is the basis of some of the most successful propositional satisfiability solvers to date. Although originally devised as a proof-procedure for first-order logic, it has been used almost exclusively for propositional logic so far because of its highly inefficient treatment of quantifiers, based on instantiation into ground formulas.

The recent FDPLL calculus by Baumgartner was the first successful attempt to lift the procedure to the first-order level without recurring to ground instantiations. FDPLL lifts to the first-order case the core of the DPLL procedure, the splitting rule, but ignores other aspects of the procedure that, although not necessary for completeness, are crucial for its effectiveness in practice.

In this paper, we present a new calculus loosely based on FDPLL that lifts these aspects as well. In addition to being a more faithful litfing of the DPLL procedure, the new calculus contains a more systematic treatment of universal literals, one of FDPLL's optimizations, and so has the potential of leading to much faster implementations.

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. In this “Slicing Information Technology tool”, documents are decomposed (“sliced”) into small units. A particular application 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.

Beyond solving the task at hand as such, with this work we contribute to the quest for arguments in favor of automated deduction techniques in the “real world”. Also, we argue why we think that automated deduction techniques are the best choice here.

The DPLL procedure, due to Davis, Putnam, Logemann, and Loveland, is the basis of some of the most successful propositional satisfiability solvers to date. Although originally devised as a proof-procedure for first-order logic, it has been used almost exclusively for propositional logic so far because of its highly inefficient treatment of quantifiers, based on instantiation into ground formulas.

The recent FDPLL calculus by Baumgartner was the first successful attempt to lift the procedure to the first-order level without recurring to ground instantiations. FDPLL lifts to the first-order case the core of the DPLL procedure, the splitting rule, but ignores other aspects of the procedure that, although not necessary for completeness, are crucial for its effectiveness in practice.

In this paper, we present a new calculus loosely based on FDPLL that lifts these aspects as well. In addition to being a more faithful litfing of the DPLL procedure, the new calculus contains a more systematic treatment of universal literals, one of FDPLL's optimizations, and so has the potential of leading to much faster implementations.