We present a polynomial resolution-based decision procedure for the recently introduced description logic ELHOVn(⊓), which features nominal schemas as new language construct. Our algorithm is based on ordered resolution and positive superposition, together with a lifting lemma. In contrast to previous work on resolution for description logics, we have to overcome the fact that ELHOVn(⊓) does not allow for a normalization resulting in clauses of globally limited size.
& Hitzler, P.
(2013). A Resolution Procedure for Description Logics with Nominal Schemas. Lecture Notes in Computer Science, 7774, 1-16.