Terminating Tableaux for SOQ with Number Restrictions on Transitive Roles

Abstract. 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.

• Type: Journal
• Year: 2009
• Where: DLOG
• Authors: Mark Kaminski, Gert Smolka
• Keywords: Automated Reasoning, Description Logic Soq, DLOG 2009, Terminating Tableau Calculus, Transitive Roles