Skip navigation
Skip navigation

ExpTime Tableaux for ALC Using Sound Global Caching

Gore, Rajeev; Nguyen, Linh Anh

Description

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
URI: http://hdl.handle.net/1885/51632
Source: Journal of Automated Reasoning
DOI: 10.1007/s10817-011-9243-0

Download

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:  17 November 2022/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator