Living Without Beth and Craig: Explicit Definitions and Interpolants in Description Logics with Nominals (Extended Abstract)

Abstract

The Craig Interpolation Property (CIP) for first-order logic (FO) states that an implication ' ) is valid in FO iff there exists a formula in FO using only the common symbols of ' and such that ' ) and ) are both valid. is then called an interpolant for ' ) . The CIP of FO and numerous other logics is generally regarded as one of the most important and useful results in formal logic, with numerous applications [39]. Description logics (DLs) are no exception; indeed, the CIP has been intensively investigated [10, 37, 25, 11, 30, 20]. A particularly important consequence of the CIP is the projective Beth definability property (PBDP), which states that a relation or constant is implicitly definable iff it is explicitly definable. In other words, a relation or constant is uniquely determined by a theory iff there exists a definition for it in that theory. The PBDP has been used in ontology engineering to extract equivalent acyclic terminologies from ontologies [10, 11], it has been investigated in ontologybased data management to equivalently rewrite ontology-mediated queries [37], and it has been proposed to support the construction of alignments between ontologies [20]. The CIP is often used as a tool to compute explicit definitions [10, 11]. It is also the basic logical property that ensures the robust behaviour of ontology modules [24]. In the form of parallel interpolation it has been investigated in [25] to decompose ontologies. In [30], it is used to study P/NP dichotomies in ontology-based query answering. The PBDP is also related to the computation of referring expressions in linguistics [28] and in ontology-based data management [7]. In this case, the focus is on computing an explicit definition (or description) for an individual rather than for arbitrary concepts. More recently, it has been observed that the CIP is closely related to the existence of strongly separating concepts for positive and negative examples given as data items in a knowledge base [13, 21, 22]. The CIP and PBDP are so powerful because intuitively very hard existence questions are reduced to straightforward deduction questions: an interpolant

-

exists iff an implication is valid and an explicit definition exists iff a straightforward formula stating implicit definability is valid. The existence problems are thus not harder than validity. For example, in the DL ALC, the existence of an interpolant or an explicit definition can be decided in ExpTime simply because deduction in ALC is in ExpTime (and without ontology even in PSpace).

Unfortunately, the CIP and the PBDP do not always hold. Particularly important examples of failure are DLs with nominals (or, equivalently, hybrid modal logics that add nominals to propositional modal logic). The CIP and PBDP fail massively in these DLs as even for very simple implications such as ( a f g ! 9r:fbg) no interpolant exists. Moreover, there is no satf g u 9r:fag) v ( b isfactory way to extend the expressive power of (expressive) DLs with nominals to ensure the existence of interpolants as validity is undecidable in any extension of ALCO with the CIP [ 9 ].

The aim of this paper is to start an investigation of the complexity of deciding the existence of interpolants and explicit definitions for DLs in which this cannot be deduced using the CIP or PBDP. We start by considering ALCO and its extensions by inverse roles and/or the universal role and prove that the existence of interpolants and the existence of explicit definitions are both 2ExpTimecomplete, thus confirming the suspicion that these are much harder problems than deduction if one has to live without Beth and Craig.

The upper bound proof is based on a straightforward characterization of the non-existence of interpolants by the existence of certain bisimulations between pointed models. We then pursue a mosaic based approach by introducing mosaics that are sets of types over the input ontologies/concepts which can be satisfied in bisimilar nodes. Natural constraints for sets of such mosaics characterize when they can be linked together to construct, simultaneously, models of the input ontologies and concepts and an appropriate bisimulation between them. The double exponential upper bound is then naturally explained by the observation that there are double exponentially many mosaics. Formally, the lower bound is proved by a reduction of the word problem for exponentially space-bounded alternating Turing machines.

Related Work. The CIP and the PBDP have been investigated extensively. They have found applications in formal verification [ 34 ], theory combinations [ 12, 14, 8 ], and in database theory for query rewriting under views [ 33 ] and query reformulation and compilation [ 38, 6 ]. Of particular relevance for this work is the investigation of interpolation and definability in modal logic in general [ 32 ] and in hybrid modal logic in particular [ 1, 9 ]. Also related is work on interpolation in guarded logics [ 18, 17, 3, 5, 4 ].

Craig interpolation should not be confused with work on uniform interpolation, both in description logic [ 29, 31, 35, 26 ] and in modal logic [ 40, 27, 19 ]. 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 hardly been investigated for logics that do not enjoy the CIP or PBDP. Exceptions are linear temporal logic, LTL, for which the decidability of interpolant existence over the natural numbers has only recently been established [ 36 ] (over finite linear orderings decidability was already established in [ 15, 16 ])1 and recent decidability and complexity results for interpolant existence in the guarded fragment [ 23 ]. This is in contrast to work on uniform interpolants in description logics which has in fact focused on the existence and computation of uniform interpolants that do not always exist [ 29, 31, 35, 26 ].

The full article containing all definitions and proofs is available at [ 2 ]. 1 Note that LTL and Craig interpolation are not mentioned in [ 36, 15, 16 ]. Using the fact that regular languages are projectively LTL definable and that LTL and firstorder logic are equivalent over the natural numbers, it is easy to see that interpolant existence is the same problem as separability of regular languages in first-order logic, modulo the succinctness of the representation of the inputs.

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 ( 2020 ), available at https://arxiv.org/abs/ 2007 .02736

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

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

5. 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 )

6. 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 )

7. 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 )

8. Calvanese , D. , Ghilardi , S. , Gianola , A. , Montali , M. , Rivkin , A. : Combined Covers and Beth Definability . In: Proc. of IJCAR (I) . pp. 181 - 200 ( 2020 )

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

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

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

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

13. Funk , M. , Jung , J.C. , Lutz , C. , Pulcini , H. , Wolter , F. : Learning description logic concepts: When can positive and negative examples be separated? In: Proc. of IJCAI . pp. 1682 - 1688 ( 2019 )

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

15. Henkell , K. : Pointlike sets: the finest aperiodic cover of a finite semigroup . J. Pure Appl. Algebra 55 ( 1-2 ), 85 - 126 ( 1988 )

16. Henkell , K. , Rhodes , J. , , Steinberg , B. : Aperiodic pointlikes and beyond . Internat. J. Algebra Comput . 20 ( 2 ), 287 - 305 ( 2010 )

17. Hoogland , E. , Marx , M. : Interpolation and definability in guarded fragments . Studia Logica 70 ( 3 ), 373 - 409 ( 2002 )

18. Hoogland , E. , Marx , M. , Otto , M. : Beth definability for the guarded fragment . In: Proc. of LPAR . pp. 273 - 285 . Lecture Notes in Computer Science, Springer ( 1999 )

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

20. 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 )

21. Jung , J.C. , Lutz , C. , Pulcini , H. , Wolter , F. : Logical separability of incomplete data under ontologies . In: Proc. of KR ( 2020 )

22. Jung , J.C. , Lutz , C. , Pulcini , H. , Wolter , F. : Separating positive and negative data examples by concepts and formulas: The case of restricted signature . In: https://arxiv.org/abs/ 2007 .02736 ( 2020 )

23. Jung , J.C. , Wolter , F. : Living without Beth and Craig: Explicit definitions and interpolants in the guarded fragment ( 2020 ), available at http://arxiv.org/abs/ 2007 .01597

24. 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 )

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

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

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

28. Krahmer , E., van Deemter, K. : Computational generation of referring expressions: A survey . Computational Linguistics 38 ( 1 ), 173 - 218 ( 2012 )

29. 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 )

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

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

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

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

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

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

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

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

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

39. Van Benthem , J.: The many faces of interpolation . Synthese pp. 451 - 460 ( 2008 )

40. 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 )