Combining Horn rules and description logics in CARIN

We describe carin , a novel family of representation languages, that combine the expressive power of Horn rules and of description logics. We address the issue of providing sound and complete inference procedures for such languages. We identify existential entailment as a core problem in reasoning in carin , and describe an existential entailment algorithm for the ALCNR description logic. As a result, we obtain a sound and complete algorithm for reasoning in non-recursive carin ALCNR knowledge bases, and an algorithm for rule subsumption over ALCNR . We show that in general, the reasoning problem for recursive carin - ALCNR knowledge bases is undecidable, and identify the constructors of ALCNR causing the undecidability. We show two ways in which carin - ALCNR knowledge bases can be restricted while obtaining sound and complete reasoning.