ExpTime tableaux with global state caching for the description logic SHIO
We give the first ExpTime(complexity-optimal) tableau decision procedure for checking satisfiability of a knowledge base in the description logic SHIO SHIO , which extends the basic description logic ALC ALC with transitive roles, hierarchies of roles, inverse roles and nominals. Our procedure exploits global state caching and does not use blind (analytic) cuts.
tableaux global state caching description logics automated reasoning