Publication details

Saarland University Computer Science

Terminating Tableaux for SOQ with Number Restrictions on Transitive Roles

Mark Kaminski, Gert Smolka

TCS 2010, Vol. 323 of IFIP AICT, pp. 213-228, Springer, September 2010

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.

DOI: 10.1007/978-3-642-15240-5_16

Download PDF        Show BibTeX               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009