Horn DLs have been introduced as syntactically de ned fragments of standard DLs that fall within the Horn fragment of rst-order logic (henceforth Horn FO) and for which ontology-mediated query answering is in PTime for data complexity [7, 8]. One possible way of de ning the concepts C of the basic fragment hornALC of ALC is by the following rule:
where A ranges over concept names and L over E L concepts. The modal logic
corresponding to hornALC was introduced independently with the aim of capturing
the intersection of Horn FO and modal logic [
A Horn simulation game is a two player game on the disjoint union of two
interpretations that di ers from the standard bisimulation or Ehrenfeucht-Frasse
game in the following respects: (1) positions in the game consist of pairs (X; b)
with a set X of nodes and a node b (which re ects that Horn languages are not
closed under disjunction); (2) a Horn simulation game uses as a subgame the
basic simulation game for checking indistinguishability by E L. Both conditions
have important consequences. The latter means that Horn simulation games are
modular as far as the characterization of the left-hand side of implications is
concerned. For example, this modularity is used to also characterize a proper
extension, hornALCr, of hornALC with the operators rR:C = 9R:> u 8R:C
(or rp = >^ p in modal logic) on the left-hand side of hornALC implications,
which also lies in Horn FO. The consequences of (1) are three-fold. First, using
sets rather than nodes in positions implies that the obvious algorithm checking
the existence of Horn simulations containing a pair (fag; b) of nodes runs in
exponential time. Thus, using Horn simulation games to check whether two nodes
a and b satisfy the same hornALC-concepts or whether two models satisfy the
same TBox axioms yields exponential time algorithms. We show that this is
unavoidable by proving corresponding ExpTime lower bounds. Second, as player 2
does not have a winning strategy in position (X; b) in the Horn simulation game
if, and only if, there exists a hornALC-concept that is true at all nodes in X
? F. Papacchini was supported by the EPSRC UK projects EP/R026084 and EP/R026173
but not true at b, our complexity results are directly applicable to the concept
learning by example (CBE ) problem: given a data set, and sets P and N of
positive and negative examples, does there exist a hornALC-concept C separating
P from N over the data? The goal of this supervised learning problem is to
automatically derive new concept descriptions from labelled data. It has been
investigated before in DL [
In the second part of the paper, we consider the guarded fragment, GF, of FO and introduce its Horn fragment hornGF. hornGF captures hornALC and many popular extensions thereof, such as inverse roles or the universal role. We generalize Horn simulations to guarded Horn simulations, and show an Ehrenfeucht-Frasse type de nability result for hornGF. This result is used to prove an ExpTime upper bound for model indistinguishability in hornGF. We also show that hornGF captures more of the intersection of ALC and Horn FO than hornALC but does not capture the intersection of GF and Horn FO. Finally, we show expressive completeness of hornGF: an FO-formula is equivalent to a hornGF-formula just in case it is preserved under guarded Horn simulations. Our proof uses in nitary methods and thus the moves of player 1 are restricted to intersections of FO- GF Horn FO de nable sets. It remains open whether the expressive completeness holds ALC GF \ Horn FO without this restriction and whether it holds in the nite model theory set- ALC \ Horn FO hornGF ting. The emerging landscape of the fragments of Horn FO and GF is de- hornALCr ALC \ hornGF picted in the right lattice of languages hornALCr \ hornGF and their intersections (modulo equivalence) where all inclusions are proper. hornALC