Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

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               

@INPROCEEDINGS{KaminskiSmolka09SOQ,
  title = {Terminating Tableaux for SOQ with Number Restrictions on Transitive Roles},
  author = {Mark Kaminski and Gert Smolka},
  year = {2009},
  month = {Jul},
  editor = {Bernardo Cuenca Grau and Ian Horrocks and Boris Motik and Ulrike Sattler},
  booktitle = {DL 2009},
  series = {CEUR Workshop Proceedings},
  volume = {477},
}

Login to edit