Sciweavers

19
Voted
DLOG
2009

Terminating Tableaux for SOQ with Number Restrictions on Transitive Roles

13 years 3 months ago
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.
Mark Kaminski, Gert Smolka
Added 17 Feb 2011
Updated 17 Feb 2011
Type Journal
Year 2009
Where DLOG
Authors Mark Kaminski, Gert Smolka
Comments (0)