Terminating Tableaux for SOQ with Number Restrictions on Transitive Roles.
Mark Stefan Kaminski, Gert Smolka · 2009
Abstract. We show that the description logic SOQ with number re-strictions on transitive roles is decidable by a terminating tableau cal-culus. The language decided by the calculus includes the universal role, which allows us to internalize TBox axioms. Termination of the system is achieved through pattern-based blocking. 1