TY - GEN
T1 - EXPTIME tableaux with global caching for description logics with transitive roles, inverse roles and role hierarchies
AU - Goré, Rajeev
AU - Nguyen, Linh Anh
PY - 2007
Y1 - 2007
N2 - The description logic SHI extends the basic description logic ALC with transitive roles, role hierarchies and inverse roles. The known tableau-based decision procedure [9] for SHI exhibit (at least) NEXP-TIME behaviour even though SHI is known to be EXPTIME-complete. The automata-based algorithms for SHI often yield optimal worst-case complexity results, but do not behave well in practice since good optimisations for them have yet to be found. We extend our method for global caching in ALC to SHI by adding analytic cut rules, thereby giving the first EXPTIME tableau-based decision procedure for SHI, and showing one way to incorporate global caching and inverse roles.
AB - The description logic SHI extends the basic description logic ALC with transitive roles, role hierarchies and inverse roles. The known tableau-based decision procedure [9] for SHI exhibit (at least) NEXP-TIME behaviour even though SHI is known to be EXPTIME-complete. The automata-based algorithms for SHI often yield optimal worst-case complexity results, but do not behave well in practice since good optimisations for them have yet to be found. We extend our method for global caching in ALC to SHI by adding analytic cut rules, thereby giving the first EXPTIME tableau-based decision procedure for SHI, and showing one way to incorporate global caching and inverse roles.
UR - http://www.scopus.com/inward/record.url?scp=35148874041&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-73099-6_12
DO - 10.1007/978-3-540-73099-6_12
M3 - Conference contribution
SN - 9783540730989
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 133
EP - 148
BT - Automated Reasoning with Analytic Tableaux and Related Methods - 16th International Conference, TABLEAUX 2007, Proceedings
PB - Springer Verlag
T2 - 16th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2007
Y2 - 3 July 2007 through 6 July 2007
ER -