Document Type

Conference Proceeding

Publication Date



We present a tableau algorithm for the description logic ALCOV. This description logic is obtained by extending the description logic ALCO with the expressive nominal schema construct that enables DL-safe datalog with predicates of arbitrary arity to be covered within the description logic framework. The tableau algorithm provides a basis to implement a delayed grounding strategy which was not facilitated by earlier versions of decision procedures for satisfiability in expressive description logics with nominal schemas.


This paper was presented at the 6th International Conference, RR 2012, Vienna, Austria, September 10-12, 2012.

The featured PDF document is the unpublished, peer-reviewed version of this article.

The featured abstract was published in the final version of this article, which appeared in Lecture Notes in Computer Science, volume 7497 pp. 234-237 and may be found at .