A Proof Theory for DL-Lite (abstract)

In this work we propose an alternative approach to inference in DL-Lite, based on a reduction to reasoning in an extension of function-free Horn Logic (EHL). We develop a calculus for EHL and prove its soundness and completeness. We will also show how to achieve decidability by means of a specific strategy, and how alternative strategies can lead to improved results in specific cases. On the one hand, we will mimic the query-answering technique based on first computing a rewriting and then evaluating it. On the other hand, we discuss a strategy that allows one to anticipate the grounding of atoms, and that might lead to better performance in the case where the size of the TBox is not dominated by the size of the data.