Alon Levy , Marie-Christine Rousset , Combining Horn Rules and Description Logics in CARIN Artificial Intelligence 1998
Abstract: 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.