Query Conservative Extensions in Horn Description Logics with Inverse Roles?

Abstract

? Accepted for IJCAI 2017. Supported by DFG project LU 1417/2 and ERC consolidator grant 647289 `CODA'.

-

Motivated by applications in ontology-mediated querying, module extraction, and ontology versioning, we consider two kinds of convervative extensions in Horn Description Logics (DLs) with inverse roles. Our prime notion is as follows: a TBox T2 T1 is a ( ; )-query conservative extension of a TBox T1, where and are signatures, if all -queries give the same answers w.r.t. T1 and T2, for every -ABox. If this is the case, then T1 can safely be replaced by T2 in querying applications where the data uses only symbols from and the query uses only symbols from . We also study ( ; )-query entailment and ( ; )-query inseparability as generalizations of conservative extensions, please see the recent survey [ 1 ] for details.

For Horn-DLs without inverse roles, query conservative extensions can be characterized in terms of the existence of homomorphisms between universal models. The resulting characterizations provide an important foundation for decision procedures, often based on tree automata [ 1 ]. In the presence of inverse roles, however, such characterizations are only correct if we require the existence of n-bounded homomorphisms, for any n. It is not obvious how the existence of such in nite families of bounded homomorphisms can be veri ed using tree automata (or related techniques) and, consequently, decidability results for query conservative extensions in Horn-DLs with inverse roles are di cult to obtain.

In this paper, we develop decision procedures for query conservative extensions in Horn DLs with inverse roles. The main idea is to provide a characterization that is much more re ned than the usual ones, mixing unbounded and bounded homomorphisms and using unbounded ones only in places where this is strictly necessary. We can then deal with the `unbounded part' using tree automata while the `bounded part' is addressed by precomputing relevant information using a mosaic technique. In this way, we establish decidability and a 2-ExpTime upper bound for query conservative extensions in Horn-ALCHIF . Together with lower bounds from [ 2 ], we get 2-ExpTime-completeness for all fragments of Horn-ALCHIF that contain ELI or Horn-ALC. These results also apply to query entailment and inseparability.

We additionally study -deductive conservative extensions between TBoxes, that is, whether T1 and T2 entail the same concept and role inclusions as well as functionality assertions over . Our main result is that deductive conservative extensions in ELHIF ? are in 2-ExpTime and coNExpTime-hard in ELI.

References

1. Botoeva , E. , Konev , B. , Lutz , C. , Ryzhikov , V. , Wolter , F. , Zakharyaschev , M. : Inseparability and conservative extensions of description logic ontologies: A survey . In: Proc. RW ( 2016 )

2. Botoeva , E. , Lutz , C. , Ryzhikov , V. , Wolter , F. , Zakharyaschev , M. : Query-based entailment and inseparability for ALC ontologies . In: Proc. IJCAI . pp. 1001 { 1007 ( 2016 )