Using tableau to decide expressive description logics with role negation

Renate A. Schmidt, Dmitry Tishkovsky

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Abstract

    This paper presents a tableau approach for deciding description logics outside the scope of OWL DL/1.1 and current state-of-the-art tableau-based description logic systems. In particular, we define a sound and complete tableau calculus for the description logic and show that it provides a basis for decision procedures for this logic and numerous other description logics with full role negation. is the extension of with the Boolean role operators, inverse of roles, domain and range restriction operators and it includes full support for nominals (individuals). is a very expressive description logic which subsumes Boolean modal logic and the two-variable fragment of first-order logic and reasoning in it is NExpTime-complete. An important novelty is the use of a generic, unrestricted blocking rule as a replacement for standard loop checking mechanisms implemented in description logic systems. An implementation of our approach exists in the system. © 2008 Springer-Verlag Berlin Heidelberg.
    Original languageEnglish
    Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.
    Pages438-451
    Number of pages13
    Volume4825
    DOIs
    Publication statusPublished - 2007
    Event6th International Semantic Web Conference, ISWC 2007 and 2nd Asian Semantic Web Conference, ASWC 2007 - Busan
    Duration: 1 Jul 2007 → …

    Conference

    Conference6th International Semantic Web Conference, ISWC 2007 and 2nd Asian Semantic Web Conference, ASWC 2007
    CityBusan
    Period1/07/07 → …

    Keywords

    • Computer Science, Theory & Methods

    Fingerprint

    Dive into the research topics of 'Using tableau to decide expressive description logics with role negation'. Together they form a unique fingerprint.

    Cite this