ExpTime Tableaux for ALC Using Sound Global Caching

Date

Authors

Gore, Rajeev

Nguyen, Linh Anh

Publisher

Kluwer Academic Publishers

Abstract

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

Keywords

Keywords: Decision procedure; Description logic; Exptime; Global caching complexity-optimal tableaux; Modal logic; Optimisation techniques; Satisfiability; Data description; Formal languages; Formal logic; Optimization Description logic; Global caching complexity-optimal tableaux; Modal logic; Tableau-based decision procedures

URI

http://hdl.handle.net/1885/51632

Collections

ANU Research Publications

Source

Journal of Automated Reasoning

Type

Journal article

DOI

10.1007/s10817-011-9243-0

Restricted until

2037-12-31

Downloads

File

Description

01_Gore_ExpTime_Tableaux_for_ALC_Using_2011.pdf (3.08 MB)