EXPTIME tableaux for ALC using sound global caching

Rajeev Goré*, Linh Anh Nguyen

*Corresponding author for this work

    Research output: Contribution to journalConference articlepeer-review

    15 Citations (Scopus)

    Abstract

    We show that global caching can be used with propagation of both satisfiability and unsatisfiability in a sound manner to give an EXPTIME algorithm for checking satisfiability w.r.t. a TBox in the basic description logic ALC. Our algorithm is based on a simple traditional tableau calculus which builds an and-or graph where no two nodes of the graph contain the same formula set. When a duplicate node is about to be created, we use the pre-existing node as a proxy, even if the proxy is from a different branch of the tableau, thereby building global caching into the algorithm from the start. Doing so is important since it allows us to reason explicitly about the correctness of global caching. We then show that propagating both satisfiability and unsatisfiability via the and-or structure of the graph remains sound. In the longer paper, by combining global caching, propagation and cutoffs, our framework reduces the search space more significantly than the framework of [1]. Also, the freedom to use arbitrary search heuristics significantly increases its application potential. A longer version with all optimisations is currently under review for a journal. An extension for SHI will appear in TABLEAUX 2007.

    Original languageEnglish
    Pages (from-to)299-306
    Number of pages8
    JournalCEUR Workshop Proceedings
    Volume250
    Publication statusPublished - 2007
    Event20th International Workshop on Description Logics, DL 2007 - Brixen/Bressanone, Italy
    Duration: 8 Jun 200710 Jun 2007

    Fingerprint

    Dive into the research topics of 'EXPTIME tableaux for ALC using sound global caching'. Together they form a unique fingerprint.

    Cite this