Affiliations: Institute of Informatics, University of Warsaw, Banacha 2, 02-097 Warsaw, Poland; and Faculty of Information Technology, VNU University of Engineering and Technology, 144 Xuan Thuy, Hanoi, Vietnam. nguyen@mimuw.edu.pl | Institute of Philosophy, University of Warsaw, Krakowskie Przedmieście 3, 00-927 Warsaw, Poland. j.golinska@uw.edu.pl
Note: [] Address for correspondence: Institute of Informatics, University of Warsaw, 02-097 Warsaw, Poland
Abstract: We present the first tableau method with an EXPTIME (optimal) complexity for checking satisfiability of a knowledge base in the description logic ${\cal{SHOQ}}$, which extends ${\cal{ALC}}$ with transitive roles, hierarchies of roles, nominals and qualified number restrictions. The complexity is measured using unary representation for numbers (in number restrictions). Our procedure is based on global caching and integer linear feasibility checking.
Keywords: automated reasoning, description logics, global state caching, integer linear feasibility
