COMBINING HORN RULES AND DESCRIPTION LOGICS IN CARIN

We describe CARIN, a novel family of representation languages, that co mbine the expressive power of Horn rules and of description logics. We address the issue of providing sound and complete inference procedure s for such languages. We identify existential entailment as a core pro blem in reasoning in CARIN, and describe an existential entailment alg orithm for the ALCNR description logic. As a result, we obtain a sound and complete algorithm for reasoning in non-recursive CARIN-ALCNR kno wledge bases, and an algorithm for rule subsumption over ALCNR. We sho w that in general, the reasoning problem for recursive CARIN-ALCNR kno wledge bases is undecidable, and identify the constructors of ALCNR ca using the undecidability. We show two ways in which CARIN-ALCNR knowle dge bases can be restricted while obtaining sound and complete reasoni ng. (C) 1998 Elsevier Science B.V. All rights reserved.