An abstract tableau calculus for the description logic SHOI using unrestricted blocking and rewriting

Mohammad Khodadadi, Renate A. Schmidt, Dmitry Tishkovsky

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

    33 Downloads (Pure)

    Abstract

    This paper presents an abstract tableau calculus for the description logic SHOI. SHOI is the extension of ALC with singleton concepts, role inverse, transitive roles and role inclusion axioms. The presented tableau calculus is inspired by a recently introduced tableau synthesis framework. Termination is achieved by a variation of the unrestricted blocking mechanism that immediately rewrites terms with respect to the conjectured equalities. This approach leads to reduced search space for decision procedures based on the calculus. We also discuss restrictions of the application of the blocking rule by means of additional side conditions and/or additional premises.
    Original languageEnglish
    Title of host publicationCEUR Workshop Proceedings|CEUR Workshop Proc.
    PublisherRWTH Aachen University
    Pages224-234
    Number of pages10
    Volume846
    Publication statusPublished - 2012
    Event25th International Workshop on Description Logics, DL 2012 - Rome
    Duration: 1 Jul 2012 → …

    Publication series

    NameCEUR Workshop Proceedings

    Conference

    Conference25th International Workshop on Description Logics, DL 2012
    CityRome
    Period1/07/12 → …

    Fingerprint

    Dive into the research topics of 'An abstract tableau calculus for the description logic SHOI using unrestricted blocking and rewriting'. Together they form a unique fingerprint.

    Cite this