Contributions:
2001
V. Haarslev and R. Möller. The Description Logic ALCNHR+ Extended with Concrete Domains: A Practically Motivated Approach. In R. Goré, A. Leitsch, and T. Nipkow, editors, International Joint Conference on Automated Reasoning, IJCAR'2001, June 18-23, Siena, Italy, pages 29–44. Springer-Verlag, 2001.
Bibtex entry Paper (PDF) ©Springer-Verlag
Abstract
The paper introduces the description logic ALCNHR+(D)-. Prominent language features beyond conjunction, full negation and quantifiers, are number restrictions, role hierarchies, transitively closed roles, generalized concept inclusions and concrete domains. As in other languages based on concrete domains (e.g. ALC(D)) a so-called predicate exists restriction concept constructor is provided. However, compared to ALC(D) only features and no feature chains are allowed in this operator. This results in a limited expressivity w.r.t. concrete domains but is required to ensure the decidability of the language. We show that the results can be exploited for building practical description logic systems for solving e.g. configuration problems.
V. Haarslev and R. Möller.
Description of the RACER System and its Applications.
In Proceedings International Workshop on Description Logics (DL-2001),
Stanford, USA, 1.-3. August, pages 131–141, 2001.
Bibtex entry Paper (PDF)
Abstract
RACER implements a TBox and ABox reasoner for the logic SHIQ. RACER was the first full-fledged ABox description logic system for a very expressive logic and is based on optimized sound and complete algorithms.
V. Haarslev and R. Möller.
High Performance Reasoning with Very Large Knowledge Bases: A Practical
Case Study.
In B. Nebel, editor, Proceedings of Seventeenth International JointÊ
Conference on Artificial Intelligence, IJCAI-01, pages 161–166, 2001.
Bibtex entry Paper (PDF)
Abstract
In this contribution we present an empirical analysis of optimization techniques devised to speed up the so-called TBox classification supported by description logic systems which have to deal with very large knowledge bases (e.g. containing more than 100,000 concept introduction axioms). These techniques are integrated into the RACE architecture which implements a TBox and ABox reasoner for the description logic ALCNHR+. The described techniques consist of adaptions of previously known as well as new optimization techniques for efficiently coping with these kinds of very large knowledge bases. The empirical results presented in this paper are based on experiences with an ontology for the Unified Medical Language System and demonstrate a considerable runtime improvement. They also indicate that appropriate description logic systems based on sound and complete algorithms can be particularly useful for large but simple knowledge bases.
V. Haarslev and R. Möller.
Optimizing Reasoning in Description Logics with Qualified Number
Restrictions.
In Proceedings International Workshop on Description Logics (DL-2001),
Stanford, USA, 1.-3. August, pages 142–151, 2001.
Bibtex entry Paper (PDF)
Abstract
In this paper an optimization technique, the so-called signature calculus, for reasoning with number restrictions in description logics is investigated. The calculus is used to speed-up ABox (and TBox) reasoning in the description logic ALCQHR+.
V. Haarslev and R. Möller.
RACER System Description.
In R. Goré, A. Leitsch, and T. Nipkow, editors, International Joint
Conference on Automated Reasoning, IJCAR'2001, June 18-23, Siena, Italy,
pages 701–705. Springer-Verlag, 2001.
Bibtex entry Paper (PDF) ©Springer-Verlag
Abstract
RACER implements a TBox and ABox reasoner for the logic SHIQ. RACER was the first full-fledged ABox description logic system for a very expressive logic and is based on optimized sound and complete algorithms. RACER also implements a decision procedure for modal logic satisfiability problems (possibly with global axioms).
V. Haarslev and R. Möller.
RACER User's Guide and Reference Manual Version 1.6.
Technical report, University of Hamburg, Computer Science Department, 2001.
Bibtex entry Paper (PDF)
V. Haarslev, R. Möller, and A.Y. Turhan.
Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive
Description Logics.
In R. Goré, A. Leitsch, and T. Nipkow, editors, International Joint
Conference on Automated Reasoning, IJCAR'2001, June 18-23, Siena, Italy,
pages 29–44. Springer-Verlag, 2001.
Bibtex entry Paper (PDF) ©Springer-Verlag
Abstract
This paper investigates optimization techniques and data structures exploiting the use of so-called pseudo models. These techniques are applied to speed-up TBox and ABox reasoning for the description logics ALCNHR+ and ALC(D). The advances are demonstrated by an empirical analysis using the description logic system RACE that implements TBox and ABox reasoning for ALCNHR+.
V. Haarslev, M. Timmann, and R. Möller.
Combining Tableaux and Algebraic Methods for Reasoning with Qualified
Number Restrictions.
In Proceedings International Workshop on Description Logics (DL-2001),
Stanford, USA, 1.-3. August, pages 152–161, 2001.
Bibtex entry Paper (PDF)
V. Haarslev, M. Timmann, and R. Möller.
Combining Tableaux and Algebraic Methods for Reasoning with Qualified
Number Restrictions.
In Proceedings of the International Workshop on Methods for Modalities 2
(M4M-2), Amsterdam, Netherlands, November 29-30, 2001.
Bibtex entry Paper (PDF)
Abstract
The paper investigates an optimization technique for reasoning with qualiȚed number restrictions in the description logic ALCQHR+ (a.k.a. SHQ), which can be seen as one of the cornerstones for reasoning technology in the context of, for instance, the semantic web activity. We present a hybrid architecture where a standard tableaux calculus is combined with a procedure deciding the satisȚability of linear inequations derived from qualiȚed number restrictions. The advances are demonstrated by an empirical evaluation using the description logic systemÊ RACER . The evaluation demonstrates a dramatic speed up compared to other known approaches.
R. Möller.
Expressive Description Logics: Foundations for Practical Applications,
Habilitation Thesis.
University of Hamburg, Computer Science Department, July 2001.
Bibtex entry Paper (PDF)