Publication details

Saarland University Computer Science

Terminating Tableaux for SOQ with Number Restrictions on Transitive Roles

Mark Kaminski, Gert Smolka

DL 2009, Vol. 477 of CEUR Workshop Proceedings, July 2009

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


Webmaster, Wed Sep 16 10:47:00 2009