We provide a model-theoretic characterization of the expressive power of Horn-ALC, the Horn fragment of the basic expressive DL ALC. We introduce Horn simulations between interpretations and show that an ALC concept is equivalent to a Horn-ALC concept i it is preserved under Horn simulations. Using the fact that ALC concepts are the bisimulation invariant fragment of FO [2], it also follows that a FO formula '(x) is equivalent to a Horn-ALC concept i it is preserved under Horn-simulations. We also extend this result to characterize Horn-ALC TBoxes via preservation under global Horn simulations. Horn DLs were introduced in [9] and since then they have been investigated extensively by the DL community [10, 11, 5, 15, 12, 1, 3, 4, 6, 7, 14, 8]. Horn modal formulas were introduced and investigated in [17]. Once restricted to ALC, these notions are equivalent to the following de nition. Let E LU concepts L be de ned by the rule L; L0 ::= > j A j L u L0 j L t L0 j 9r:L, where A ranges of concept names and r over role names. Then Horn-ALC concepts R are de ned by the rule R; R0 ::= ? j > j :A j A j R u R0 j L ! R j 9r:R j 8r:R where A ranges over concept names, r over role names, and L is an E LU concept. A Horn-ALC TBox is a nite set of concept inclusions of the form > v R. For a binary relation R and sets X; Y , we set XR"Y if for all d 2 X there exists d0 2 Y with (d; d0) 2 R and we set XR#Y if for all d0 2 Y there exists d 2 X with (d; d0) 2 R. Let I and J be interpretations. We write (I; d) sim (J ; e) if there is a simulation between I and J containing (d; e). E LU concepts are preserved under simulations in the sense that (I; d) sim (J ; e) and d 2 CI imply e 2 CI , for all E LU concepts C. De nition 1 (Horn Simulation). Let I and J be interpretations. A Horn simulation between I and J is a relation Z P( I ) J such that if X Z d then X 6= ; and the following hold: (A) if X Z d and X AI , then d 2 AJ , for all A 2 NC; (F) if X Z d and X(rI )"Y , then there exist Y 0 Y and d0 2 (d; d0) 2 rJ and Y 0 Z d0, for all r 2 NR; (B) if X Z d and (d; d0) 2 rJ , then there exists Y Y Z d0, for all r 2 NR; (S) (J ; d) sim (I; x) for all x 2 X. (I; X) is Horn-simulated by (J ; d), in symbols (I; X) horn (J ; d), if there exists a Horn simulation Z between I and J such that X Z d.
Horn simulations di er from standard bisimulations in at least two respects: they are non-symmetric and they relate sets to points (rather than points to points). They also employ as a `subgame' the standard simulation game. The de nition of Horn simulations is inspired by games used to provide van Benthem style characterizations of concepts in weak DLs such as F L [13]. We also use the obvious depth k approximation of Horn simulations.
An ALC concept C is preserved under (k-)Horn simulations if for all (I; X) and (J ; d), X CI and (I; X) (hko)rn (J ; d) imply d 2 CJ .
Theorem 1. Let C be an ALC concept of depth k. Then the following conditions are equivalent: 1. C is equivalent to a Horn-ALC concept; 2. C is preserved under Horn simulations; 3. C is preserved under k-Horn simulations.
The proof is inspired by Otto's nitary proofs of (extensions of) van Benthem's bisimulation characterization of modal logic via nitary bisimulations [16]. Theorem 1 can be lifted to characterize Horn-ALC TBoxes via preservation under global (k-)Horn simulations.
Theorem 1 allows us to show that Horn-ALC does not capture the intersection of ALC and Horn FO. For example, the ALC concept C = ((9s:>)u((Eu8s:A) ! D)) is not preserved under Horn simulations. In fact, for the interpretations I0 and J0, and the Horn simulation Z de ned in the gure below, fa; dg CI0 but a0 62 CJ0 . Thus, C is not equivalent to any Horn-ALC concept. C is, however, equivalent to the Horn FO formula 9y (s(x; y) ^ (:E(x) _ :A(y) _ D(x))).
E; D
a s
s b :A
I0 c A
E; :D
d s e A
J0 E; :D a0 s b0 A The full paper is available at https://cgi.csc.liv.ac.uk/ frank/publ/publ.html. The authors were supported by EPSRC UK grant EP/M012646/1. 3. Bienvenu, M., Hansen, P., Lutz, C., Wolter, F.: First order-rewritability and containment of conjunctive queries in horn description logics. In: Proceedings of the Twenty-Fifth International Joint Conference on Arti cial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016. pp. 965{971 (2016) 4. Botoeva, E., Kontchakov, R., Ryzhikov, V., Wolter, F., Zakharyaschev, M.: Games for query inseparability of description logic knowledge bases. Artif. Intell. 234, 78{ 119 (2016) 5. Eiter, T., Gottlob, G., Ortiz, M., Simkus, M.: Query answering in the description logic horn-SHIQ. In: Logics in Arti cial Intelligence, 11th European Conference, JELIA 2008, Dresden, Germany, September 28 - October 1, 2008. Proceedings. pp. 166{179 (2008) 6. Glimm, B., Kazakov, Y., Tran, T.: Ontology materialization by abstraction renement in horn SHOIF. In: Proceedings of the Thirty-First AAAI Conference on Arti cial Intelligence, February 4-9, 2017, San Francisco, California, USA. pp. 1114{1120 (2017) 7. Gutierrez-Basulto, V., Jung, J.C., Sabellek, L.: Reverse engineering queries in ontology-enriched systems: The case of expressive horn description logic ontologies. In: Proceedings of IJCAI-ECAI-18. AAAI Press (2018) 8. Hernich, A., Lutz, C., Papacchini, F., Wolter, F.: Horn-rewritability vs ptime query evaluation in ontology-mediated querying. In: Proceedings of IJCAI-ECAI. AAAI Press (2018) 9. Hustadt, U., Motik, B., Sattler, U.: Data complexity of reasoning in very expressive description logics. In: IJCAI. pp. 466{471 (2005) 10. Kazakov, Y.: Consequence-driven reasoning for Horn-SHIQ ontologies. In:
Boutilier, C. (ed.) IJCAI. pp. 2040{2045 (2009) 11. Krotzsch, M.: Description Logic Rules, Studies on the Semantic Web, vol. 8. IOS
Press (2010), https://doi.org/10.3233/978-1-61499-342-1-i
12. Krotzsch, M., Rudolph, S., Hitzler, P.: Complexities of horn
description logics. ACM Trans. Comput. Log. 14(
Methods in Computer Science 13(4) (2017)
15. Ortiz, M., Rudolph, S., Simkus, M.: Query answering in the Horn fragments of the
description logics SHOIQ and SROIQ. In: IJCAI. pp. 1039{1044 (2011)
16. Otto, M.: Modal and guarded characterisation theorems over nite transition
systems. Ann. Pure Appl. Logic 130(