Description logics (DLs) are a family of knowledge representation languages which can be used to represent the terminological knowledge of an application domain in a structured and formally well-understood way. DLs can be used, for example, for conceptual modeling or as ontology languages. In fact, OWL (Web Ontology Language), recommended by W3C, is based on description logics. In the current paper we give the first direct ExpTime (optimal) tableau decision procedure, which is not based on transformation or on the pre-completion technique, for checking satisfiability of a knowledge base in the description logic . Our procedure uses sound global caching and can be implemented as an extension of the highly optimized tableau prover TGC to obtain an efficient program for the mentioned satisfiability problem. © 2010 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Nguyen, L. A., & Szałas, A. (2010). Tableaux with global caching for checking satisfiability of a knowledge base in the description logic SH. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6220 LNCS, pp. 21–38). https://doi.org/10.1007/978-3-642-15034-0_2
Mendeley helps you to discover research relevant for your work.