We show that the description logic SOQ with number restrictions on transitive roles is decidable by a terminating tableau calculus. 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.
The version at CEUR-WS.org contains some buggy definitions that are fixed in this version.
Download PDF Show BibTeX
Login to edit