Beth De?nability in Expressive Description Logics Balder ten Cate? Enrico Franconi I?nanc? Seylan†
Abstract
The Beth de?nability property, a well-known property from classical logic, is investigated in the context of description logics (DLs): if a general L TBox implicitly de?nes an L -concept in terms of a given signature, where L is a DL, then does there always exist over this signature an explicit de?nition in L for the concept? This property has been studied before and used to optimize reasoning in DLs. In this paper a complete classi?cation of Beth de?nability is provided for extensions of the basic DL ALC with transitive roles, inverse roles, role hierarchies, and/or functionality restrictions, both on arbitrary and on ?nite structures. Moreover, we present a tableau-based algorithm which computes explicit de?nitions of at most double exponential size. This algorithm is optimal because it is also shown that the smallest explicit de?nition of an implicitly de?ned concept may be double exponentially long in the size of the input TBox. Finally, if explicit de?nitions are allowed to be expressed in ?rst-order logic then we show how to compute them in E XP T IME.