Optimised Reasoning for SHIQ

Ian HorrocksIan Horrocks, Ulrike SattlerUlrike Sattler

Datei:HorrocksSattler-LTCS-01-08.ps.gz

Download

Ian Horrocks, Ulrike Sattler
Optimised Reasoning for SHIQ
Technical Report, LuFG Theoretical Computer Science, RWTH Aachen, volume LTCS-01-08, 2001. LTCS-Report

Details
Bibtex

KurzfassungAbstract
The tableau algorithm implemented in the FaCT knowledge representation system decides satisfiability and subsumption in SHIQ, a very expressive description logic providing, e.g., inverse and transitive roles, number restrictions, and general axioms. Intuitively, the algorithm searches for a tree-shaped abstraction of a model. To ensure termination of this algorithm without compromising correctness, it stops expanding paths in the search tree using a so-called ``double-blocking condition. This condition was clearly more exacting than was strictly necessary, but it was assumed that more precisely defined blocking conditions would, on the one hand, make the proof of the algorithm's correctness far more difficult and, on the other hand (and more importantly), be so costly to check as to outweigh any benefit that might be derived. However, FaCT's failure to solve UML derived knowledge bases led us to reconsider this conjecture and to formulate more precisely defined blocking conditions. We prove that the revised algorithm is still sound and complete, and demonstrate that it greatly improves FaCT's performance - in some cases by more than two orders of magnitude.
Bemerkung: Note: See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@techreport{ HorrocksSattler-LTCS-01-08,
  address = {Germany},
  author = {I. {Horrocks} and U. {Sattler}},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.},
  number = {LTCS-01-08},
  title = {Optimised Reasoning for SHIQ},
  type = {LTCS-Report},
  year = {2001},
}