Optimal Rewritings in Definitorially Complete Description Logics

In this paper, we revisit the problem of definitorial completeness, i.e., whether a given general TBox T in a description logic (DL) L can be rewritten to an acyclic TBox T in L . This is an important problem because crucial optimisations in DL reasoners rely on acyclic parts in TBoxes. It is known that such rewritings are possible for definitorial TBoxes in ALC and in logics ALCX for X {S, H, I}. Here we establish optimal bounds on the sizes of the resulting acyclic TBoxes. In particular, we reduce the known triple exponential upper bound on ALC-TBoxes to single exponential. Additionally, we prove the same upper bound for those extensions with X {S, H, I} for which there was no established result before. This means, together with the already known exponential lower bound for ALC, that our bounds are tight.

• Type: Journal
• Year: 2010
• Where: DLOG
• Authors: Inanç Seylan, Enrico Franconi, Jos de Bruijn
• Keywords: Acyclic Tbox, Automated Reasoning, DLOG 2010, Exponential Upper Bound, Upper Bound