ExpTime Tableaux with Global Caching for the Description Logic SHOQ
Logic in Computer Science
2014-07-22 v2
Abstract
We give the first ExpTime (complexity-optimal) tableau decision procedure for checking satisfiability of a knowledge base in the description logic SHOQ, which extends the basic description logic ALC with transitive roles, hierarchies of roles, nominals and quantified number restrictions. The complexity is measured using unary representation for numbers. Our procedure is based on global caching and integer linear feasibility checking.
Keywords
Cite
@article{arxiv.1405.7221,
title = {ExpTime Tableaux with Global Caching for the Description Logic SHOQ},
author = {Linh Anh Nguyen and Joanna Golińska-Pilarek},
journal= {arXiv preprint arXiv:1405.7221},
year = {2014}
}
Comments
arXiv admin note: substantial text overlap with arXiv:1205.5838