ExpTime tableaux for ALC using sound global caching

Rajeev Goré; Linh Anh Nguyen

doi:10.1007/s10817-011-9243-0

ExpTime tableaux for ALC using sound global caching

Rajeev Goré^*, Linh Anh Nguyen

^*Corresponding author for this work

Research output: Contribution to journal › Article › peer-review

16 Citations (Scopus)

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 foundation for ExpTime (complexity-optimal) tableau-based decision procedures for many modal and description logics, to which various optimisation techniques can be applied.

Original language	English
Pages (from-to)	355-381
Number of pages	27
Journal	Journal of Automated Reasoning
Volume	50
Issue number	4
DOIs	https://doi.org/10.1007/s10817-011-9243-0
Publication status	Published - Apr 2013

Access to Document

10.1007/s10817-011-9243-0

Cite this

@article{cae61d45c8464bc4a2293d75eef6df0f,

title = "ExpTime tableaux for ALC using sound global caching",

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 foundation for ExpTime (complexity-optimal) tableau-based decision procedures for many modal and description logics, to which various optimisation techniques can be applied.",

keywords = "Description logic, Global caching complexity-optimal tableaux, Modal logic, Tableau-based decision procedures",

author = "Rajeev Gor{\'e} and Nguyen, {Linh Anh}",

year = "2013",

month = apr,

doi = "10.1007/s10817-011-9243-0",

language = "English",

volume = "50",

pages = "355--381",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

number = "4",

}

TY - JOUR

T1 - ExpTime tableaux for ALC using sound global caching

AU - Goré, Rajeev

AU - Nguyen, Linh Anh

PY - 2013/4

Y1 - 2013/4

N2 - 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 foundation for ExpTime (complexity-optimal) tableau-based decision procedures for many modal and description logics, to which various optimisation techniques can be applied.

AB - 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 foundation for ExpTime (complexity-optimal) tableau-based decision procedures for many modal and description logics, to which various optimisation techniques can be applied.

KW - Description logic

KW - Global caching complexity-optimal tableaux

KW - Modal logic

KW - Tableau-based decision procedures

UR - http://www.scopus.com/inward/record.url?scp=84876501032&partnerID=8YFLogxK

U2 - 10.1007/s10817-011-9243-0

DO - 10.1007/s10817-011-9243-0

M3 - Article

SN - 0168-7433

VL - 50

SP - 355

EP - 381

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 4

ER -

ExpTime tableaux for ALC using sound global caching

Abstract

Access to Document

Other files and links

Fingerprint

Cite this