A Proof Theory for DL-Lite

Abstract. In this work we propose an alternative approach to inference in DLLite, 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 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 propose a strategy that mimics the query-answering technique based on first computing a query rewriting and then evaluating it. On the other hand, we propose strategies that allow 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.

• Type: Conference
• Year: 2007
• Where: DLOG
• Authors: Diego Calvanese, Evgeny Kharlamov, Werner Nutt
• Keywords: Alternative Approach, Alternative Strategies, Automated Reasoning, DLOG 2007, Function-free Horn Logic