EXPTIME tableaux with global caching for description logics with transitive roles, inverse roles and role hierarchies

Rajeev Goré*, Linh Anh Nguyen

*Corresponding author for this work

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

    41 Citations (Scopus)

    Abstract

    The description logic SHI extends the basic description logic ALC with transitive roles, role hierarchies and inverse roles. The known tableau-based decision procedure [9] for SHI exhibit (at least) NEXP-TIME behaviour even though SHI is known to be EXPTIME-complete. The automata-based algorithms for SHI often yield optimal worst-case complexity results, but do not behave well in practice since good optimisations for them have yet to be found. We extend our method for global caching in ALC to SHI by adding analytic cut rules, thereby giving the first EXPTIME tableau-based decision procedure for SHI, and showing one way to incorporate global caching and inverse roles.

    Original languageEnglish
    Title of host publicationAutomated Reasoning with Analytic Tableaux and Related Methods - 16th International Conference, TABLEAUX 2007, Proceedings
    PublisherSpringer Verlag
    Pages133-148
    Number of pages16
    ISBN (Print)9783540730989
    DOIs
    Publication statusPublished - 2007
    Event16th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2007 - Aix en Provence, France
    Duration: 3 Jul 20076 Jul 2007

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume4548 LNAI
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference16th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2007
    Country/TerritoryFrance
    CityAix en Provence
    Period3/07/076/07/07

    Fingerprint

    Dive into the research topics of 'EXPTIME tableaux with global caching for description logics with transitive roles, inverse roles and role hierarchies'. Together they form a unique fingerprint.

    Cite this