Peter Baumgartner, Ulrich Furbach, and Bernd Thomas.
Model Based Deduction for Knowledge Representation.
In Bertram Fronhöfer and Steffen Hölldobler, editors, 17. WLP: Workshop Logische Programmierung, TU Dresden, December 11-13, 2002, number TUD-FI03-03 in Technische Berichte der Fakultät Informatik, pages 156-166. TU Dresden, 01062 Dresden, April 2002.
ISSN 1430-211X. [ bib | .pdf ]
Peter Baumgartner, Margret Gross-Hardt, and Anna B. Simon.
Living Book - An Interactive and Personalized Book.
In Veljko Milutinovic, editor, SSGRR 2002s - International Conference on Advances in Infrastructure for e-Business, e-Education, e-Science, and e-Medicine on the Internet. Published electronically (, 2002. [ bib | .pdf ]
In the era of information technology, providing high quality and state of the art educational material is quite a challenge and requires the use of new media. The In2Math project at the University of Koblenz-Landau develops in this context the Living Book; Living Book means personalized user oriented educational material together with interactive components. The Living Book aims at supporting the fundamental parts of undergraduate classes in theoretical computer science. The main goal is to support the active, explorative and self-determined learning in lectures, tutorials and selfstudy.

This paper describes the main aspects of the Living Book and explains the concepts and ideas behind it as well as the techniques used to realized these concepts.

Peter Baumgartner.
A First-Order Logic Davis-Putnam-Logemann-Loveland Procedure.
In Gerhard Lakemeyer and Bernhard Nebel, editors, AI in the new Millenium. Morgan Kaufmann, 2002.
This book contains the contributions to the International Joint Conference on Artificial Intelligence (IJCAI 2001) distinguished paper track.bib | .pdf ]
Peter Baumgartner and Ulrich Furbach.
Model Based Deduction for Knowledge Representation (Position Paper).
In Steffen Staab Martin Frank, Natasha Noy, editor, International Workshop on the Semantic Web, Workshop at WWW2002, 2002. [ bib ]
Peter Baumgartner.
Automatische Deduktion - Von Kalkülen zu Anwendungen.
Habilitation thesis, University of Koblenz-Landau, Germany, 2002.
(in German). [ bib ]
Peter Baumgartner.
A First-Order Logic Davis-Putnam-Logemann-Loveland Procedure.
Fachberichte Informatik 3-2002, Universität Koblenz-Landau, Universität Koblenz-Landau, Institut für Informatik, Rheinau 1, D-56075 Koblenz, 2002. [ bib | .pdf ]
The Davis-Putnam-Logemann-Loveland procedure (DPLL) was introduced in the early 60s as a proof procedure for first-order logic. Nowadays, only its propositional logic core component is widely used in efficient propositional logic provers and respective applications. This success motivates to reconsider lifting DPLL to the first-order logic level in a more contemporary way, by exploiting successful first-order techniques like “unification”. Following this idea, in this paper a first-order logic version of DPLL, FDPLL, is presented.

While propositional DPLL is based on a splitting rule for case analysis wrt. ground and complementary literals, FDPLL uses a lifted splitting rule, i.e. the case analysis is made wrt. non-ground and complementary literals now. To make this work, a new way of treating variables is employed. It comes together with a compact way of representing and reasoning with first-order logic interpretations, much like propositional DPLL reasons about propositional truth assignments. As a nice consequence, FDPLL naturally decides the class of Bernays-Schönfinkel formulas, which is notoriously difficult for most other calculi.