Peter Baumgartner and Ulrich Furbach.
Automated Deduction Techniques for the Management of Personalized Documents.
Annals of Mathematics and Artificial Intelligence - Special Issue on Mathematical Knowledge Management, 38(1), 2003. [ bib | .pdf ]
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.

 
Peter Baumgartner, Ulrich Furbach, and Margret Groß-Hardt.
Living Books.
In Wolfgang Uhr, Werner Esswein, and Eric Schoop, editors, Wirtschaftsinformatik 2003, volume 1, pages 693-706. Physica-Verlag, 2003. [ bib ]
 
Peter Baumgartner and Cesare Tinelli.
The Model Evolution Calculus.
In Baader [6], pages 350-364. [ bib | .pdf ]
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.

 
Peter Baumgartner, Ulrich Furbach, Margret Gross-Hardt, and Alex Sinner.
'Living Book' :- 'Deduction', 'Slicing', 'Interaction'. - System Description.
In Baader [6], pages 284-288. [ bib ]
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.

 
Peter Baumgartner, Ulrich Furbach, Margret Gross-Hardt, Thomas Kleemann, and Christoph Wernhard.
KRHyper Inside - Model Based Deduction in Applications.
In Proc. CADE-19 Workshop on Novel Applications of Deduction Systems, 2003. [ bib | .pdf ]
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.

 
Franz Baader, editor.
Automated Deduction - CADE-19, volume 2741 of Lecture Notes in Artificial Intelligence. Springer, 2003. [ bib ]
 
Peter Baumgartner and Hantao Zhang, editors.
First-Order Theorem Proving, volume 36 of Special issue of the Journal of Symbolic Computation. Academic Press, 2003. [ bib ]
 
Peter Baumgartner and Cesare Tinelli.
The Model Evolution Calculus.
Fachberichte Informatik 1-2003, Universität Koblenz-Landau, Universität Koblenz-Landau, Institut für Informatik, Rheinau 1, D-56075 Koblenz, 2003. [ bib | .pdf ]
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.