A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI

M Khodadadi, R A Schmidt, D Tishkovsky, Thomas Eiter (Editor), Birte Glimm (Editor), Yevgeny Kazakov (Editor), Markus Krötzsch (Editor)

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


    The paper presents a tableau calculus with several refinements for reasoning in the description logic SHOI. The calculus uses non-standard rules for dealing with TBox statements. Whereas in existing tableau approaches a fixed rule is used for dealing with TBox statements, the tableau calculus uses a dynamically generated set of refined rules. This approach has become practical because reasoners with flexible sets of rules can be generatedwith the tableau prover generation prototype MetTeL. We also define and investigate variations of the unrestricted blocking mechanism in which equality reasoning is realised by ordered rewriting and the application of the blocking rule is controlled by excluding its application to a fixed, finite set of individual terms. Reasoning with the unique name assumption and excluding ABox individuals from the application of blocking can be seen as two separate instances of the latter. Experiments show the refinements lead to fewer rule applications and improved performance.
    Original languageEnglish
    Title of host publicationProceedings of the 26th International Workshop on Description Logics (DL-2013)
    EditorsThomas Eiter, Birte Glimm, Yevgeny Kazakov, Markus Krötzsch
    PublisherRWTH Aachen University
    Number of pages11
    Publication statusPublished - 2013

    Publication series

    NameCEUR Workshop Proceedings


    Dive into the research topics of 'A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI'. Together they form a unique fingerprint.

    Cite this