ExpTime Tableaux for ALC Using Sound Global Caching

Date

2011

Authors

Gore, Rajeev
Nguyen, Linh Anh

Journal Title

Journal ISSN

Volume Title

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

Description

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

Citation

Source

Journal of Automated Reasoning

Type

Journal article

Book Title

Entity type

Access Statement

License Rights

DOI

10.1007/s10817-011-9243-0

Restricted until

2037-12-31