Franz Baader

See: Description Logics, Modal Logics, Automated Deduction, Term Rewriting, Unification Theory.

References

(Baader et al., 2008) ⇒ Franz Baader, Sebastian Brandt, and Carsten Lutz. (2008). “Pushing the EL Envelope Further.” In: Proceedings of the OWLED 2008 DC Workshop on OWL: Experiences and Directions.

(Baader et al., 2005) ⇒ Franz Baader, Sebastian Brandt, and Carsten Lutz. (2005). “Pushing the EL Envelope.” In: Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence (IJCAI 2005).
- ABSTRACT: Recently, it has been shown that the small description logic (DL) EL, which allows for conjunction and existential restrictions, has better algorithmic properties than its counterpart FL0, which allows for conjunction and value restrictions. Whereas the subsumption problem in FL0 becomes already intractable in the presence of acyclic TBoxes, it remains tractable in EL even with general concept inclusion axioms (GCIs). On the one hand, we extend the positive result for EL by identifying a set of expressive means that can be added to EL without sacrificing tractability. On the other hand, we show that basically all other additions of typical DL constructors to EL with GCIs make subsumption intractable, and in most cases even EXPTIME-complete. In addition, we show that subsumption in FL0 with GCIs is EXPTIME-complete.

(Baader & Nipkow, 1999) ⇒ Franz Baader, and Tobias Nipkow. (1999). “Term Rewriting and All That." Cambridge University Press. ISBN:0521779200
- BOOK OVERVIEW: This textbook offers a unified, self-contained introduction to the field of term rewriting. Baader and Nipkow cover all the basic material--abstract reduction systems, termination, confluence, completion, and combination problems--but also some important and closely connected subjects: universal algebra, unification theory, Gröbner bases, and Buchberger's algorithm. They present the main algorithms both informally and as programs in the functional language Standard ML (An appendix contains a quick and easy introduction to ML). Key chapters cover crucial algorithms such as unification and congruence closure in more depth and develop efficient Pascal programs. The book contains many examples and over 170 exercises. This is also an ideal reference book for professional researchers: results spread over many conference and journal articles are collected here in a unified notation, detailed proofs of almost all theorems are provided, and each chapter closes with a guide to the literature.