Cut-Free ExpTime Tableaux for Checking Satisfiability of a Knowledge Base in the Description Logic SHI
Logic in Computer Science
2012-07-17 v2
Abstract
We give the first cut-free ExpTime (optimal) tableau decision procedure for checking satisfiability of a knowledge base in the description logic SHI, which extends the description logic ALC with transitive roles, inverse roles and role hierarchies.
Keywords
Cite
@article{arxiv.1106.2305,
title = {Cut-Free ExpTime Tableaux for Checking Satisfiability of a Knowledge Base in the Description Logic SHI},
author = {Linh Anh Nguyen},
journal= {arXiv preprint arXiv:1106.2305},
year = {2012}
}
Comments
a long version of the paper "Linh Anh Nguyen. A Cut-Free ExpTime Tableau Decision Procedure for the Description Logic SHI. In Proceedings of ICCCI'2011, LNAI 6922, pages 572-581, Springer-Verlag, 2011", 27 pages