Description Logics and the Two-Variable Fragment
Carsten Lutz, Ulrike Sattler, Frank Wolter · 2001
We present a description logic L that is as expressive as the twovariable fragment of first-order logic and differs from other logics with this property in that it encompasses solely standard role- and conceptforming operators. The description logic L is obtained from ALC by adding full Boolean operators on roles, the inverse operator on roles and an identity role. It is proved that L has the same expressive power as the two-variable fragment FO of first-order logic by presenting a translation -formulae into equivalent L-concepts (and back). Additionally, we discuss an interesting complexity phenomenon: both L and FO are NExpTime-complete and so is the restriction of FO to finitely many relation symbols; astonishingly, the restriction of L to a bounded number of role names is in ExpTime.