Skip navigation
Skip navigation

ExpTime Tableaux for ALC Using Sound Global Caching

Gore, Rajeev; Nguyen, Linh Anh


We present a simple ExpTime (complexity-optimal) tableau decision procedure based on and-or graphs with sound global caching for checking satisfiability of a concept w.r.t. a TBox in $\mathcal{ALC}$. Our algorithm is easy to implement and provides a found

CollectionsANU Research Publications
Date published: 2011
Type: Journal article
Source: Journal of Automated Reasoning
DOI: 10.1007/s10817-011-9243-0


File Description SizeFormat Image
01_Gore_ExpTime_Tableaux_for_ALC_Using_2011.pdf3.15 MBAdobe PDF    Request a copy

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

Updated:  20 July 2017/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator