Interpolants and Explicit Definitions in Horn Description Logics (Extended Abstract)

Abstract

The projective Beth definability property (PBDP) of a description logic (DL) L states that a concept or individual name is explicitly definable under an Lontology O by an L-concept using symbols from a signature if, and only if, it is implicitly definable by under O. The importance of the PBDP for DL research stems from the fact that it provides a polynomial time reduction of the problem of deciding the existence of an explicit definition to subsumption checking and the usefulness of having explicit definitions for numerous knowledge engineering tasks, including the equivalent rewritability of ontology-mediated queries, the construction of alignments between ontologies, the computation of referring expressions, the extraction of equivalent acyclic terminologies from ontologies, and the decomposition of ontologies [11,33,26,22,12,19,3]. The PBDP is often investigated in tandem with the Craig interpolation property (CIP) which states that if an L-concept is subsumed by another L-concept under some L-ontology then one finds an interpolating L-concept using the shared symbols of the two input concepts only. In fact, the CIP implies the PBDP and the interpolants obtained using the CIP can serve as explicit definitions.1 Many standard Boolean DLs such as ALC, ALCI, ALCQI, and their extensions with transitive roles enjoy the CIP and PBDP and sophisticated algorithms for computing interpolants and explicit definitions have been developed in the context of DLs, modal logic, and the guarded fragment [12,28,14,6]. Important exceptions are the extensions of any of the above DLs with nominals and/or role hierarchies [12]. In fact, it has recently been shown that the problem of deciding the existence of an interpolant/explicit definition becomes 2ExpTimecomplete for DLs such as ALC with nominals and ALC with role hierarchies which is in sharp contrast to the ExpTime-completeness of the same problem for ALC itself inherited from the ExpTime-completeness of subsumption under ALC-ontologies [2]. The aim of this paper is to determine which Horn-DLs enjoy the CIP/PBDP, investigate the complexity of deciding the existence of interpolants/explicit definitions for those that do not enjoy it, and establish bounds on the size of interCopyright c 2021 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). 1 We use the definition of the CIP for DLs introduced in [12] according to which a DL enjoys the CIP if for any ontologies O1 and O2 and concepts C1; C2 in the DL such that O1 [ O2 j= C1 v C2, there exists a concept D in the DL using symbols shared by O1; C1 and O2; C2 such that O1 [ O2 j= C1 v D and O1 [ O2 j= D v C2.

-

polants/explicit definitions. Rather surprisingly, it turns out that most standard Horn-DLs do not enjoy the CIP/PBDP.

Theorem 1. E L with nominals, E L with the universal role, E L with a single role inclusion of the form r s v s, E L with role hierarchies and a single transitive role, E LI, Horn-ALC, and Horn-ALCI do not enjoy the CIP nor PBDP.

E L and E L with role hierarchies enjoy the CIP and PBDP.

The result for E L with nominals has been proved in [ 3 ] already and the positive result for E L and E L with role hierarchies in [ 22,26 ]. It follows that the behaviour of Horn-DLs is entirely different from Boolean DLs: adding role hierarchies to ALC does not preserve the CIP/PBDP [ 21 ] but it does for E L. On the other hand, extending ALC with the universal role and/or inverse roles preserves the CIP/PBDP, but it does not for E L.

We note that in Theorem 1, the CIP and PBDP for Horn-L with L 2 fALC; ALCIg can be naturally defined in two different ways, depending on the language for interpolants/explicit definitions. If one is interested in positive existential interpolants/definitions, then one can choose E L(I)-concepts, and if more expressive power is desired, one can choose general Horn-L-concepts. We show that in fact in some cases only Horn-L-interpolants/explicit definitions exist, but that the CIP/PBDP fails for both E L(I)-concepts and Horn-L-concepts as interpolants/definitions.

For E L-ontologies with unrestricted role inclusions (RIs) r1 rn v r we also prove a rather general sufficient condition for the existence of explicit definitions: if O is an E L-ontology with RIs such that each RI either only uses roles in or no role in , then any implicitly -definable concept name under O is also explicitly -definable under O. A similar result can be shown for interpolants.

We next determine the complexity of deciding the existence of interpolants and explicit definitions and tight bounds on their size for DLs in the E L-family of DLs.

Theorem 2. For any DL extending E L with any combination of nominals, RIs, the universal role, or ?, the existence of interpolants and explicit definitions is in PTime. If an interpolant/explicit definition exists, then there exists one of at most exponential size. This bound is optimal.

The proof is based on a careful analysis of canonical models and the introduction and analysis of derivation trees (first used in [ 8 ] for E LI) to estimate the size of interpolants. For DLs extending E LI we use tree automata and again an analysis of derivation trees to prove the following.

Theorem 3. For E LI and its extension with nominals and/or the universal role deciding the existence of interpolants and explicit definitions is ExpTimecomplete. For E LI with and without the universal role, if an interpolant/explicit definition exists, then there exists one of at most double exponential size. This bound is optimal. For E LI with nominals it remains open whether an interpolant/explicit definition of at most double exponential size exists, if one exists at all. Theorem 3 also holds for Horn-ALC and Horn-ALCI provided one asks for interpolants and explicit definitions in E LI. If one admits more expressive Horn-concepts as interpolants or explicit definitions, then the decidability and complexity of existence remains open and could be attacked using the games introduced in [ 20 ]. We finally note that for all DLs considered in this paper one always finds an interpolant in the Horn fragment of first-order logic which is known to enjoy the CIP and PBDP.

We conclude with a brief description of related work. The CIP and PBDP have been investigated extensively. They have found applications in formal verification [ 30 ], theory combinations [ 13,15 ], and in database theory for query rewriting under views [ 29 ] and query reformulation and compilation [ 35,7 ]. Of particular relevance for this work is the investigation of interpolation and definability in modal logic in general [ 28 ] and in hybrid modal logic in particular [ 1,10 ]. Also related is work on interpolation in guarded logics [ 17,16,4,6,5 ].

The main aim of this paper is to investigate explicit definability of concept names under Horn-DL ontologies. We have therefore chosen a definition of Craig interpolation and interpolants that generalizes the projective Beth definability property and explicit definability in a natural and useful way, following [ 12 ]. There are, however, other notions of Craig interpolation that are of interest and have been investigated. Of particular importance for modularity and various other purposes is the following version: if O is an ontology and C v D an inclusion such that O j= C v D, then there exists an ontology O0 in the shared signature of O and C v D such that O j= O j 0 = C v D. This property has been considered for E L and various extensions in [ 34,22 ]. Currently, it is unknown whether any general results can be proved about the relationship between this version of the Craig interpolation property, the version considered in this article, and/or the projective Beth definability property.

Craig interpolation should not be confused with work on uniform interpolation, both in description logic [ 25,27,31,23 ] and in modal logic [ 36,24,18 ]. Uniform interpolants generalize Craig interpolants in the sense that a uniform interpolant is an interpolant for a fixed antecedent and any formula implied by the antecedent and sharing with it a fixed set of symbols.

Interpolant and explicit definition existence have only recently been investigated for logics that do not enjoy the CIP or PBDP. In description logic, the work of [ 2 ] on Boolean DLs with nominals and role hierarchies was discussed above. Explicit definition existence is also investigated in [ 3 ] for the case in which one is interested in the explicit definition of nominals, see also [ 9 ]. In [ 20 ], interpolant and explicit definition existence are investigated for the guarded and two-variable fragments, proving that the problems becomes harder than validity. The interpolant existence problem for linear temporal logic LTL is considered in [ 32 ].

The full version of this paper is available at https://www.csc.liv.ac.uk/ ~frank/publ/publ.html.

References

1. Areces , C. , Blackburn , P. , Marx , M. : Hybrid logics: Characterization, interpolation and complexity . J. Symb. Log . 66 ( 3 ), 977 - 1010 ( 2001 )

2. Artale , A. , Jung , J.C. , Mazzullo , A. , Ozaki , A. , Wolter , F. : Living without Beth and Craig: Explicit definitions and interpolants in description logics with nominals and role hierarchies . In: Proc. of AAAI ( 2021 )

3. Artale , A. , Mazzullo , A. , Ozaki , A. , Wolter , F. : On free description logics with definite descriptions . In: Proc. of KR ( 2021 )

4. Bárány , V. , Benedikt , M. , ten Cate , B. : Some model theory of guarded negation . J. Symb. Log . 83 ( 4 ), 1307 - 1344 ( 2018 )

5. Benedikt , M. , ten Cate , B. , Vanden Boom , M. : Interpolation with decidable fixpoint logics . In: Proc. of LICS . pp. 378 - 389 . IEEE Computer Society ( 2015 )

6. Benedikt , M. , ten Cate , B. , Vanden Boom , M. : Effective interpolation and preservation in guarded logics . ACM Trans. Comput. Log . 17 ( 2 ), 8: 1 - 8 : 46 ( 2016 )

7. Benedikt , M. , Leblay , J., ten Cate , B. , Tsamoura , E.: Generating Plans from Proofs: The Interpolation-based Approach to Query Reformulation . Synthesis Lectures on Data Management , Morgan & Claypool Publishers ( 2016 )

8. Bienvenu , M. , Lutz , C. , Wolter , F. : First-order rewritability of atomic queries in Horn description logics . In: Proc. of IJCAI ( 2013 )

9. Borgida , A. , Toman , D. , Weddell , G.E. : On referring expressions in query answering over first order knowledge bases . In: Proc. of KR . pp. 319 - 328 ( 2016 )

10. ten Cate , B. : Interpolation for extended modal languages . J. Symb. Log . 70 ( 1 ), 223 - 234 ( 2005 )

11. ten Cate , B. , Conradie , W. , Marx , M. , Venema , Y. : Definitorially complete description logics . In: Proc. of KR . pp. 79 - 89 . AAAI Press ( 2006 )

12. ten Cate , B. , Franconi , E. , Seylan , İ.: Beth definability in expressive description logics . J. Artif. Intell. Res . 48 , 347 - 414 ( 2013 )

13. Cimatti , A. , Griggio , A. , Sebastiani , R.: Interpolant generation for UTVPI . In: Proc. of CADE . pp. 167 - 182 . Springer ( 2009 )

14. Fitting , M. , Kuznets , R.: Modal interpolation via nested sequents . Ann. Pure Appl. Log . 166 ( 3 ), 274 - 305 ( 2015 )

15. Goel , A. , Krstic , S. , Tinelli , C. : Ground interpolation for combined theories . In: Proc. of CADE . pp. 183 - 198 . Springer ( 2009 )

16. Hoogland , E. , Marx , M. : Interpolation and definability in guarded fragments . Stud. Log . 70 ( 3 ), 373 - 409 ( 2002 )

17. Hoogland , E. , Marx , M. , Otto , M. : Beth definability for the guarded fragment . In: Proc. of LPAR . pp. 273 - 285 . Springer ( 1999 )

18. Iemhoff , R.: Uniform interpolation and the existence of sequent calculi . Annals of Pure and Applied Logic 170 ( 11 ), 102711 ( 2019 )

19. Jiménez-Ruiz , E. , Payne , T.R. , Solimando , A. , Tamma , V.A.M.: Limiting logical violations in ontology alignnment through negotiation . In: Proc. of KR . pp. 217 - 226 . AAAI Press ( 2016 )

20. Jung , J.C. , Wolter , F. : Living without Beth and Craig: Definitions and interpolants in the guarded and two-variable fragments . In: Proc. of LICS ( 2021 )

21. Konev , B. , Lutz , C. , Walther , D. , Wolter , F. : Formal properties of modularisation . In: Modular Ontologies, Lecture Notes in Computer Science , vol. 5445 , pp. 25 - 66 . Springer ( 2009 )

22. Konev , B. , Lutz , C. , Ponomaryov , D.K. , Wolter , F. : Decomposing description logic ontologies . In: Proc. of KR . AAAI Press ( 2010 )

23. Koopmann , P. , Schmidt , R.A. : Uniform interpolation and forgetting for ALC ontologies with aboxes . In: Proc. of AAAI . pp. 175 - 181 . AAAI Press ( 2015 )

24. Kowalski , T. , Metcalfe , G.: Uniform interpolation and coherence . Annals of pure and applied logic 170(7) , 825 - 841 ( 2019 )

25. Lutz , C. , Seylan , I. , Wolter , F. : An automata-theoretic approach to uniform interpolation and approximation in the description logic EL . In: Proc. of KR . AAAI Press ( 2012 )

26. Lutz , C. , Seylan , I. , Wolter , F. : The data complexity of ontology-mediated queries with closed predicates . Logical Methods in Computer Science 15 ( 3 ) ( 2019 )

27. Lutz , C. , Wolter , F. : Foundations for uniform interpolation and forgetting in expressive description logics . In: Proc. of IJCAI . pp. 989 - 995 . IJCAI/AAAI ( 2011 )

28. Maksimova , L. , Gabbay , D. : Interpolation and Definability in Modal and Intuitionistic Logics . Clarendon Press ( 2005 )

29. Marx , M. : Queries determined by views: Pack your views . In: Proc. of PODS . p. 23 - 30 . ACM ( 2007 )

30. McMillan , K.L. : Interpolation and sat-based model checking . In: Proc. of CAV . pp. 1 - 13 . Springer ( 2003 )

31. Nikitina , N. , Rudolph , S. : (Non-)succinctness of uniform interpolants of general terminologies in the description logic EL . Artif. Intell . 215 , 120 - 140 ( 2014 )

32. Place , T. , Zeitoun , M. : Separating regular languages with first-order logic . Log. Methods Comput. Sci . 12 ( 1 ) ( 2016 )

33. Seylan , I. , Franconi , E., de Bruijn , J.: Effective query rewriting with ontologies over dboxes . In: Proc. of IJCAI . pp. 923 - 925 ( 2009 )

34. Sofronie-Stokkermans , V. : Interpolation in local theory extensions . Log. Methods Comput. Sci. 4 ( 4 ) ( 2008 ). https://doi.org/10.2168/LMCS-4( 4 :1) 2008 , https: //doi.org/10.2168/LMCS-4( 4 :1) 2008

35. Toman , D. , Weddell , G.E. : Fundamentals of Physical Design and Query Compilation . Synthesis Lectures on Data Management , Morgan & Claypool Publishers ( 2011 )

36. Visser , A. , et al.: Uniform interpolation and layered bisimulation . In: Gödel'96: Logical foundations of mathematics, computer science and physics-Kurt Gödel's legacy , pp. 139 - 164 . Association for Symbolic Logic ( 1996 )