A Proof Theory for DL-Lite (summary)

The idea of using ontologies as a conceptual view over data repositories is becoming more and more popular. In practice, ontologies mediate between the repositories and a user, which allows the user to query the repositories by posing queries to the ontologies. Since data in the repositories is typically of a very large volume (much larger than the ontology itself), query answering should be efficient on the data. At present the standard ontology language is OWL, but none of its variants (OWL Full/DL/Lite) satisfies this efficiency requirement. In order to solve this problem, a new ontology language, called DL-Lite, was proposed; the language is a fragment of OWL Lite and allows for efficient query answering. In fact, DL-Lite is a family of various Description Logics, where DL-Lite(F) and DL-Lite(R) are the ones best studied to date.

We investigate two aspects of DL-Lite(F): properties of models of DL-Lite(F) knowledge bases (KBs) and a calculus for the logic. As it is shown by Calvanese&al06, in general DL-Lite(F) KBs have neither finite nor least (wrt inclusion) models. We construct examples to illustrate these phenomenons. We introduce the notion of a universal model for a KB (which is based on the notion of a universal solution proposed in Fagin&al05) and show that any satisfiable DL-Lite(F) KB has a universal model. We also show that a chase of a knowledge base is a universal model.

Answering queries over a KB requires in principle to evaluate the query over all models of the KB. We show that for answering conjunctive queries (CQs) over a DL-Lite(F) KB it suffices to evaluate it only over a universal model of the KB, and consequently, over a chase of the KB. In general the chases of a KB may be infinite. We identify (using results from Fagin&al05) a class of KBs for which all chases are finite and, moreover, CQs can be answered in polynomial time.

However, it turns out that, also for KBs that have an infinite chase, it is possible to answer CQs in finite time. Calvanese at al. do this in Calvanese&al05 by presenting a query rewriting algorithm (with Logspace data complexity) that takes as input a KB and a CQ and rewrite the query to a union of CQs which is then evaluated over the data stored in the KB in order to return all answers. We do this by defining a calculus that takes as input a KB and a CQ and allows one to derive all answers. We show how the algorithm presented by Calvanese&al05 can be obtained by imposing a specific control strategy on the calculus. Finally, we present a way proposed in Calvanese&al06 to reduce several other reasoning tasks for DLs to answering CQs, so that it shows the calculus and the algorithm can be applied to a wide range of inferences.