Abstract
We study the problem of updates for TBoxes represented in Description Logics of the DL-Lite family. DL-Lite is at the basis of OWL 2 QL, one of the tractable fragments of OWL 2, the recently proposed revision of the Web Ontology Language. In this paper, we address for the first time the problem of updating TBoxes. We propose some principles that TBox updates should respect. We review known model- and formula-based approaches for updates of logical theories, and exhibit limitations of model-based approaches to handle TBox updates. We propose a novel formula-based approach, and present a polynomial time algorithm to compute TBox updates for DL-LiteFR . We also study the relationship between propositional logic satisfiability for Horn clauses and computation of TBox updates for DL-Lite.