Tractable Reasoning in Description Logics with Functionality Constraints

Ontological query answering amounts to returning the answers to a query, that are logically entailed by the union of a set of membership assertions and an ontology, where the latter is a set of logical assertions. Ontological query answering has applications, for instance, in the Semantic Web and in semantic data integration. We propose as ontology language a new description logic, called DLR

±

, allowing for roles of arbitrary arity and role inclusion assertions with permutation, as well as functionality assertions, which generalizes the most widely-adopted tractable ontology languages. The interaction between functionality assertions and other constructs in ontology languages has been shown to lead easily to intractability and even undecidability. The absence of such interaction is characterized by

separability

, a semantic property which has been studied in different contexts. With the aim of finding expressive ontology languages that are also tractable, we give a precise characterization of separable DLR

±

ontologies by providing a syntactic condition that is necessary and sufficient for separability. We also present an exhaustive complexity analysis of reasoning, here intended as conjunctive query answering and satisfiability checking, under separable DLR

±

ontologies.