A Tableau Algorithm for Description Logics with Nominal Schemas

TitleA Tableau Algorithm for Description Logics with Nominal Schemas
Publication TypeConference Papers
Year of Publication2012
AuthorsKrisnadhi, A, Hitzler, P
EditorKrötzsch, M, Straccia, U
Conference NameWeb Reasoning and Rule Systems, 6th International Conference, RR2012, Vienna, Austria, September 10-12, 2012, Proceedings
Date Published09/2012

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.

Refereed DesignationRefereed