A Resolution Procedure for Description Logics with Nominal Schemas

Authors

Cong Wang
Pascal HitzlerFollow

Document Type

Conference Proceeding

Publication Date

2013

Abstract

We present a polynomial resolution-based decision procedure for the recently introduced description logic ELHOV_n(⊓), 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 ELHOV_n(⊓) does not allow for a normalization resulting in clauses of globally limited size.

Comments

Attached is the unpublished, peer-reviewed version of the proceeding. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-37996-3_1.

Presented at the Second Joint International Conference on Semantic Technology, Nara, Japan, December 2-4, 2012.

Repository Citation

Wang, C., & Hitzler, P. (2013). A Resolution Procedure for Description Logics with Nominal Schemas. Lecture Notes in Computer Science, 7774, 1-16.
https://corescholar.libraries.wright.edu/cse/179

DOI

10.1007/978-3-642-37996-3_1