ExpTime Tableaux for the Description Logic SHIQ Based on Global State Caching and Integer Linear Feasibility Checking
Logic in Computer Science
2014-01-03 v4
Abstract
We give the first ExpTime (complexity-optimal) tableau decision procedure for checking satisfiability of a knowledge base in the description logic SHIQ when numbers are coded in unary. Our procedure is based on global state caching and integer linear feasibility checking.
Cite
@article{arxiv.1205.5838,
title = {ExpTime Tableaux for the Description Logic SHIQ Based on Global State Caching and Integer Linear Feasibility Checking},
author = {Linh Anh Nguyen},
journal= {arXiv preprint arXiv:1205.5838},
year = {2014}
}