A Proof Theory for DL-Lite

Diego Calvanese, Evgeny Kharlamov, and Werner Nutt

Proc. of the 20th Int. Workshop on Description Logics (DL 2007). Volume 250 of CEUR Workshop Proceedings, http://ceur-ws.org/. 2007.

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.


@inproceedings{DL-2007-proof-theory,
   title = "A Proof Theory for DL-Lite",
   year = "2007",
   author = "Diego Calvanese and Evgeny Kharlamov and Werner Nutt",
   booktitle = "Proc. of the 20th Int. Workshop on Description Logics
(DL 2007)",
   pages = "235--242",
   volume = "250",
   series = "CEUR Workshop Proceedings, http://ceur-ws.org/",
}
pdf url