P.: A tableau algorithm for description logics with nominal schemas

Abstract. 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 ba-sis 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.