01139nas a2200169 4500008004100000245006800041210006600109260002200175300001200197490000900209520056900218100002100787700002000808700002200828700002200850856009700872 2012 eng d00aA Tableau Algorithm for Description Logics with Nominal Schemas0 aTableau Algorithm for Description Logics with Nominal Schemas bSpringerc09/2012 a234-2370 v74973 a

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.

1 aKrisnadhi, Adila1 aHitzler, Pascal1 aKrötzsch, Markus1 aStraccia, Umberto uhttps://daselab.cs.ksu.edu/publications/tableau-algorithm-description-logics-nominal-schemas