=Paper=
{{Paper
|id=Vol-2211/paper-46
|storemode=property
|title=A Van Benthem Theorem for Horn Description and Modal Logic
|pdfUrl=https://ceur-ws.org/Vol-2211/paper-46.pdf
|volume=Vol-2211
|authors=Fabio Papacchini,Frank Wolter
|dblpUrl=https://dblp.org/rec/conf/dlog/PapacchiniW18
}}
==A Van Benthem Theorem for Horn Description and Modal Logic==
https://ceur-ws.org/Vol-2211/paper-46.pdf
A Van Benthem Theorem for Horn Description
and Modal Logic (Extended Abstract)
Fabio Papacchini and Frank Wolter
University of Liverpool, UK, {papacchf,wolter}@liverpool.ac.uk
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 iff 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 iff 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 definition. Let ELU concepts L be defined
by the rule L, L0 ::= > | A | L u L0 | L t L0 | ∃r.L, where A ranges of concept
names and r over role names. Then Horn-ALC concepts R are defined by the
rule
R, R0 ::= ⊥ | > | ¬A | A | R u R0 | L → R | ∃r.R | ∀r.R
where A ranges over concept names, r over role names, and L is an ELU concept.
A Horn-ALC TBox is a finite 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 ∈ X there
exists d0 ∈ Y with (d, d0 ) ∈ R and we set XR↓ Y if for all d0 ∈ Y there exists
d ∈ X with (d, d0 ) ∈ 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). ELU concepts
are preserved under simulations in the sense that (I, d) sim (J , e) and d ∈ C I
imply e ∈ C I , for all ELU concepts C.
Definition 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 ∈ AJ , for all A ∈ NC ;
(F) if X Z d and X(rI )↑ Y , then there exist Y 0 ⊆ Y and d0 ∈ ∆J such that
(d, d0 ) ∈ rJ and Y 0 Z d0 , for all r ∈ NR ;
(B) if X Z d and (d, d0 ) ∈ rJ , then there exists Y ⊆ ∆I with X(rI )↓ Y and
Y Z d0 , for all r ∈ NR ;
(S) (J , d) sim (I, x) for all x ∈ 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 differ 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
definition of Horn simulations is inspired by games used to provide van Benthem
style characterizations of concepts in weak DLs such as FL− [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)
(k)
and (J , d), X ⊆ C I and (I, X) horn (J , d) imply d ∈ C J .
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 finitary proofs of (extensions of) van Ben-
them’s bisimulation characterization of modal logic via finitary bisimulations [16].
Theorem 1 can be lifted to characterize Horn-ALC TBoxes via preservation un-
der 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 = ((∃s.>)u((Eu∀s.A) →
D)) is not preserved under Horn simulations. In fact, for the interpretations I0
and J0 , and the Horn simulation Z defined in the figure below, {a, d} ⊆ C I0 but
a0 6∈ C J0 . Thus, C is not equivalent to any Horn-ALC concept. C is, however,
equivalent to the Horn FO formula ∃y (s(x, y) ∧ (¬E(x) ∨ ¬A(y) ∨ D(x))).
I0 J0
E, D E, ¬D E, ¬D
a d a0
s s s s
b c e b0
¬A A A 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.
References
1. Baader, F., Bienvenu, M., Lutz, C., Wolter, F.: Query and predicate emptiness in
ontology-based data access. J. Artif. Intell. Res. (JAIR) 56, 1–59 (2016)
2. van Benthem, J.: Modal Logic and Classical Logic. Bibliopolis (1983)
3. Bienvenu, M., Hansen, P., Lutz, C., Wolter, F.: First order-rewritability and con-
tainment of conjunctive queries in horn description logics. In: Proceedings of the
Twenty-Fifth International Joint Conference on Artificial 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 Artificial 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 re-
finement in horn SHOIF. In: Proceedings of the Thirty-First AAAI Conference
on Artificial Intelligence, February 4-9, 2017, San Francisco, California, USA. pp.
1114–1120 (2017)
7. Gutiérrez-Basulto, V., Jung, J.C., Sabellek, L.: Reverse engineering queries in
ontology-enriched systems: The case of expressive horn description logic ontolo-
gies. 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. Krötzsch, 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. Krötzsch, M., Rudolph, S., Hitzler, P.: Complexities of horn de-
scription logics. ACM Trans. Comput. Log. 14(1), 2:1–2:36 (2013),
http://doi.acm.org/10.1145/2422085.2422087
13. Kurtonina, N., de Rijke, M.: Expressiveness of concept expressions in first-order
description logics. Artif. Intell. 107(2), 303–333 (1999)
14. Lutz, C., Wolter, F.: The data complexity of description logic ontologies. Logical
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 finite transition sys-
tems. Ann. Pure Appl. Logic 130(1-3), 173–205 (2004)
17. Sturm, H.: Modal horn classes. Studia Logica 64(3), 301–313 (2000)