Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

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               

@INPROCEEDINGS{KaminskiSmolka:2010:SOQ,
  title = {Terminating Tableaux for SOQ with Number Restrictions on Transitive Roles},
  author = {Mark Kaminski and Gert Smolka},
  year = {2010},
  month = {Sep},
  editor = {Cristian S. Calude and Vladimiro Sassone},
  publisher = {Springer},
  booktitle = {TCS 2010},
  series = {{IFIP} {AICT}},
  volume = {323},
  pages = {213-228},
}

Login to edit