An ExpTime Tableau Method for Dealing with Nominals and Quantified Number Restrictions in Deciding the Description Logic SHOQ.
Linh Anh Nguyen, Joanna Golińska‐Pilarek · 2013
Abstract. We present the first tableau method with an ExpTime (optimal) complexity for checking satisfiability of a knowledge base in the description logic SHOQ, which extends ALC with transitive roles, hierarchies of roles, nominals and quantified number restrictions. The complexity is measured using binary representation for numbers. Our procedure is based on global caching and integer linear feasibility checking. 1