A proof theory for DL-Lite
MetadataShow full item record
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 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.