LATPub651: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Marcel Lippmann (Diskussion | Beiträge) KKeine Bearbeitungszusammenfassung |
Marcel Lippmann (Diskussion | Beiträge) KKeine Bearbeitungszusammenfassung |
||
| (2 dazwischenliegende Versionen desselben Benutzers werden nicht angezeigt) | |||
| Zeile 1: | Zeile 1: | ||
{{Publikation Erster Autor | {{Publikation Erster Autor | ||
|ErsterAutorVorname= | |ErsterAutorVorname=Ian | ||
|ErsterAutorNachname=Horrocks | |ErsterAutorNachname=Horrocks | ||
|FurtherAuthors= | |FurtherAuthors=Ulrike Sattler | ||
}} | }} | ||
{{Techreport | {{Techreport | ||
| Zeile 15: | Zeile 15: | ||
}} | }} | ||
{{Publikation Details | {{Publikation Details | ||
|Abstract=The tableau algorithm implemented in the FaCT knowledge | |Abstract=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. | ||
|ISBN= | |ISBN= | ||
|ISSN= | |ISSN= | ||
| Zeile 56: | Zeile 34: | ||
year = {2001}, | year = {2001}, | ||
} | } | ||
}} | }} | ||
Aktuelle Version vom 25. März 2015, 16:34 Uhr
Optimised Reasoning for SHIQ
Ian HorrocksIan Horrocks, Ulrike SattlerUlrike Sattler
Ian Horrocks, Ulrike Sattler
Optimised Reasoning for SHIQ
Technical Report, LuFG Theoretical Computer Science, RWTH Aachen, volume LTCS-01-08, 2001. LTCS-Report
Optimised Reasoning for SHIQ
Technical Report, LuFG Theoretical Computer Science, RWTH Aachen, volume LTCS-01-08, 2001. LTCS-Report
- 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},
}
