Skip navigation
Skip navigation

EXPTIME tableaux for ALC using sound global caching

Gore, Rajeev; Nguyen, Linh Anh


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...[Show more]

CollectionsANU Research Publications
Date published: 2007
Type: Conference paper
Source: 2007 International Workshop on Description Logics Proceedings


File Description SizeFormat Image
01_Gore_EXPTIME_tableaux_for_ALC_using_2007.pdf164.93 kBAdobe PDF    Request a copy

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  12 November 2018/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator