Constructive Interpolation and Concept-Based Beth Definability for Description Logics via Sequents

1 Introduction

Defining new concepts in terms of given concepts and relations is an important operation within the context of description logics (DLs), and logic more generally. Typically, a new concept NewC can be defined in one of two ways: (1) implicitly, by specifying a set of axioms such that the interpretation of NewC is uniquely determined by the interpretation of the given concepts and relations, or (2) explicitly, by writing a definition NewC ≡ D where NewC does not appear in D. Description logics for which implicit definability implies explicit definability are said to be definitorially complete [Baader and Nutt, 2003; ten Cate et al., 2006], or to exhibit the concept-based Beth definability property (CBP) [ten Cate et al., 2013]. This is Beth's definability property [Beth, 1956] from first-order logic rephrased for DLs.

Beth definability and variations thereof have found numerous applications in DLs. For example, the property has been used in ontology engineering to extract acyclic terminologies from general ones [Baader and Nutt, 2003; ten Cate et al., 2006]. This is of particular importance since reasoning with acyclic terminologies is usually less complex than with general ones, e.g. satisfiability over acyclic ALC-terminologies is PSPACE-complete while being EXPTIME-complete over general ALC-terminologies [Donini, 2003]. Other applications include, rewriting ontology-mediated queries [Franconi and Kerhet, 2019; Seylan et al., 2009; Toman and Weddell, 2022], learning concepts separating positive and negative examples [Artale et al., 2023; Funk et al., 2019], and computing referring expressions, which is of value in computational linguistics and data management [Areces et al., 2008; Borgida et al., 2016; Artale et al., 2021].

A number of methods have been used to confirm the existence of, or actually compute, explicit definitions of implicitly definable concepts for expressive DLs; e.g. model-theoretic mosaic-based methods have been employed to decide the existence of explicit definitions for ALCH, ALCO, and ALCHOI [Artale et al., 2023; Jung et al., 2022]. However, as noted in these works, these methods are non-constructive, confirming the existence of explicit definitions without necessarily providing them. Thus, interest has been expressed in developing constructive methods that actually compute explicit definitions. We note that constructive methods have been employed in the literature, e.g. methods relying on the computation of normal forms and uniform interpolants [ten Cate et al., 2006] or which compute explicit definitions using tableau-based algorithms [ten Cate et al., 2013]. With the aim of furthering this programme, we present a constructive method applicable to a large number of DLs, which computes explicit concept-based definitions of implicitly definable concepts and establishes the CBP by means of sequent systems.

Since its introduction in the 1930's, Gentzen's sequent calculus has become one of the preferred formalisms for the construction of proof calculi [Gentzen, 1935a; Gentzen, 1935b]. A sequent calculus is a set of inference rules operating over expressions (called sequents) of the form Γ ⊢ ∆ with Γ and ∆ sequences or (multi)sets of formulae. Sequent systems have found fruitful applications, being exploited in the development of automated reasoning methods [Slaney, 1997] and being used to establish non-trivial properties of logics such as consistency [Gentzen, 1935a; Gentzen, 1935b], decidability [Dyckhoff, 1992], and interpolation [Maehara, 1960]. Regarding this last point, it was first shown by Maehara that sequent systems could be leveraged to constructively prove the Craig interpolation property [Craig, 1957] of a logic. Since this seminal work, Maehara's interpolation method has been extended and adapted in a variety of ways to prove Craig interpolation for diverse classes of logics with sequent-style systems, including modal logics [Fitting and Kuznets, 2015], intermediate logics [Kuznets and Lellmann, 2018], and temporal logics [Lyon et al., 2020]. As Craig interpolation implies Beth definability, it follows that the sequent-based methodology is applicable to the latter.

In this paper, we provide the first sequent calculi for RIQontologies and show how these calculi can be used to compute interpolants, explicit definitions, and to confirm the CBP. Although our work is inspired by Maehara's method, we note that it is a non-trivial generalization of that method. As discussed in [Lyon et al., 2020], Maehara's original method is quite restricted, being inapplicable in many cases to even basic modal logics, which a fortiori means the method is inapplicable to expressive DLs. To overcome these difficulties, we use a generalized notion of sequent and interpolant that encodes a tree whose nodes are multisets of DL concepts accompanied by (in)equalities over nodes. Given a proof with such sequents, we show that all axiomatic sequents can be assigned interpolants-which are themselves sequents-and that such interpolants can be 'propagated' through the proof yielding an interpolant of the conclusion. Explicit definitions can then be readily extracted from these interpolants. We note that our method is constructive in the sense that interpolants are computed relative to a given proof of a general concept inclusion implied by a RIQ-ontology. Although such proofs are in principle computable, we left the specification of an explicit proof-search algorithm that builds such proofs to future work, noting that such algorithms can be written by adapting known techniques; e.g. [Horrocks and Sattler, 2004].

Finally, we remark that although our work shares similarities with that of [ten Cate et al., 2013], our method goes beyond this work as we establish the CBP for the highly expressive DL RIQ, and due to the modularity of our sequent systems, our method is applicable to any restriction of RIQ, e.g. logics within the FL and EL families [Donini et al., 1997; Baader et al., 2005]. By modularity we mean that the deletion of inference rules or modification of side conditions on rules allows for sequent systems to be provided for fragments of RIQ. Our work also intersects that of [ten Cate et al., 2006], which establishes the CBP for ALC extended with PUR Horn conditions, but differs both in terms of methodology and our consideration of qualified number restrictions.

Outline of Paper. In Section 2, we define the logic RIQ, define the CBP and related notions, and explicate certain grammar theoretic concepts used in formulating inference rules. In Section 3, we present our sequent systems and establish that each system enjoys fundamental properties. Section 4 develops and explains our new sequent-based method that computes explicit definitions of implicitly definable concepts and establishes the CBP, using RIQ as case study. To the best of our knowledge, this is the first proof that RIQ has the CBP. Section 5 concludes and discusses future work. Last, we remark that proofs of all results can be found in the online, appended version [Lyon and Karge, 2024].

2 Preliminaries

In the first part of this section, we introduce the language and semantics for the description logic RIQ, which subsumes various expressive and lightweight DLs [Baader et al., 2005; Calvanese and De Giacomo, 2003]. Subsequently, we discuss and define a notion of interpolation and concept-based Beth definability, which will be of pivotal interest in this paper. In the last part of this section, we introduce special types of semi-Thue systems [Post, 1947], referred to as R-systems, which are essential in the formulation of our sequent calculi.

2.1 Language and Semantics: RIQ

The description logic RIQ is defined relative to a vocabulary V = (NR,NC), which is a pair containing pairwise disjoint, countable sets. The set NR contains role names used to denote binary relations and the set NC contains concept names used to denote classes of entities. We use the (potentially annotated) symbols r, s, . . . to denote role names, and A, B, . . . to denote concept names. We define a role to be a role name or an inverse role r- such that r ∈ NR. We define the inverse of a role to be Inv(r) = r- and Inv(r-) = r given that r ∈ NR. We let R := NR ∪ {Inv(r) | r ∈ NR} denote the set of roles. A complex role inclusion axiom (RIA) is an expression r1 ◦ · · · ◦ rn ⊑ s such that r1, . . . , rn and s are roles, and ◦ denotes the usual composition operation over binary relations; we assume n-ary compositions r1 ◦ · · · ◦ rn associate to the left. We define an RBox R to be a finite collection of RIAs. As identified by Horrocks and Sattler [Horrocks and Sattler, 2004], to ensure the decidability of reasoning with RIQ, only regular RBoxes may be used in ontologies (defined below). 1 Let ≺ be a strict partial order on the set NR of role names; we define an RIA w ⊑ r to be ≺-regular iff r is a role name, and either (1) w = rr, (2) w = r-, (3) w = s1 ◦ · · · ◦ sn and si ≺ r for all 1 ≤ i ≤ n, (4) w = r ◦ s1 ◦ · · · ◦ sn and si ≺ r for all 1 ≤ i ≤ n, or (5) w = s1 ◦ · · · ◦ sn ◦ r and si ≺ r for all 1 ≤ i ≤ n. An RBox R is defined to be regular iff a strict partial order ≺ over NR exists such that every RIA in R is ≺-regular.

We recursively define a role name r to be simple (with respect to an RBox R) iff either (1) no RIA of the form w ⊑ r occurs in R, or (2) for each s ⊑ r ∈ R, s is a simple role name or its inverse is. Also, an inverse role r- is defined to be simple if r is simple.

We define complex concepts to be formulae in negation normal form generated by the following grammar in BNF:

where A ∈ NC, ⊙ ∈ {⊔, ⊓}, Q ∈ {∃r, ∀r | r ∈ R}, s is a simple role, and n ∈ N. We use the symbols C, D, . . . (potentially annotated) to denote complex concepts. We define ⊤ = A⊔¬A and ⊥ = A⊓¬A for a fixed A ∈ NC, and define a literal L to be either a concept name or its negation, i.e. L ∈ {A, ¬A | A ∈ NC}. For a concept name A, we define ˙¬A := ¬A and ˙¬¬A := A, and we lift the definition of negation to complex concepts in the usual way, noting that ˙¬(⩽nr.C) := (⩾(n+1)r.C), and

1 Note, our interpolation results go through for general RBoxes, i.e. this restriction is not needed for the work in Sections 3 and 4.

We recursively define the weight of a concept C as follows: (1) w(L) = 1 with L ∈ {A, ¬A | A ∈ NC}, (2) w(C ⊙D) = w(C)+w(D)+1 with ⊙ ∈ {⊓, ⊔}, (3) w(Q.C) = w(C)+1 with Q ∈ {∃r, ∀r | r ∈ R}, (4) w(⩽ns.C) = w(C) + n + 1, and (5) w(⩾ns.C) = w(C) + n.

A general concept inclusion axiom (GCI) is a formula of the form C ⊑ D such that C and D are complex concepts. A TBox T is a finite set of GCIs and we make the simplifying assumption that every GCI in a TBox T is of the form⊤ ⊑ C. We define a RIQ-ontology O (which we refer to as an ontology for short) to be the union of an RBox R and TBox T , that is, O = R ∪ T . For a set X of concepts, GCIs, or RIAs, we let con(X) denote the set of all concept names occurring in X, and we let sig(X) denote the set of all concept names and roles occurring in X. Symbols from a vocabulary V are interpreted accordingly:

Definition 1 (Interpretation). An interpretation I = (∆I , ·I ) is a pair consisting of a non-empty set ∆I called the domain and a map ·I such that

• if A ∈ NC, then AI ⊆∆I with ¬AI =∆I \ AI ;
• if r ∈ NR, then rI ⊆∆I ×∆I .

We define (r-)I = {(b, a) | (a, b) ∈ rI } and interpret compositions over roles in the usual way. We lift interpretations to complex concepts accordingly:

• (C ⊔D)I = C I ∪DI ;
• (C ⊓D)I = C I ∩DI ;
• ∃r.C I = {a ∈ ∆I | ∃b ∈ ∆I , (a, b) ∈ rI & b ∈ C I };
• ∀r.C I = {a ∈ ∆I | ∀b ∈ ∆I , (a, b) ∈ rI ⇒ b ∈ C I };
• ⩽ns.C I :={a∈∆I : |{b : (a, b) ∈ sI &b ∈ C I }| ≤ n};
• ⩾ns.C I :={a∈∆I : |{b : (a, b) ∈ sI & b ∈ C I }| ≥ n}.

An interpretation satisfies C ⊑ D or r1 ◦ · · · ◦ rn ⊑ s, written I ⊨ C ⊑ D and I ⊨ r1 ◦ · · · ◦ rn ⊑ s iff C I ⊆ DI and (r1 ◦ · · · ◦ rn)I ⊆ sI , respectively. An interpretation I is defined to be a model of an ontology O, written I ⊨ O, iff it satisfies all GCIs and RIAs in O. We write O ⊨ C ⊑ D iff for every interpretation I, if I ⊨ O, then I ⊨ C ⊑ D, and we write O ⊨ C ≡ D when O ⊨ C ⊑ D and O ⊨ D ⊑ C.

2.2 Definability and Interpolation

The notion of Beth definability, first defined within the context of first-order logic [Beth, 1956], takes on a number of distinct formulations within the context of DLs. In [Baader and Nutt, 2003; ten Cate et al., 2006], Beth definability is reinterpreted as the notion of definitorial completeness, which has also been named concept-based Beth definability (CBP) [ten Cate et al., 2013]. Intuitively, a DL L has the CBP when the implicit definability of a concept C under an L-ontology O using a signature Θ = Ξ ∪ NR with Ξ ⊆ con(C, O) implies its explicit definability using symbols from Θ. This is distinct from the projective Beth definability property (PBDP), which is defined in the same way but relative to a signature Θ ⊆ sig(C, O), or the weaker Beth definability property (BDP) where the signature Θ is the set of all symbols distinct from the concept defined [Artale et al., 2023]. In this paper, we focus on the CBP, and leave the investigation of sequentbased methodologies for establishing other definability properties to future work. Let us now formally define the CBP.

Let L be a DL, C be a complex concept in L, O an Lontology, and Θ ⊆ con(C, O). 2 We define C to be implicitly concept-definable from Θ under O iff for any two models I and J of O such that ∆I = ∆J and for each P ∈ Θ ∪ NR, P I = P J , it follows that C I = C J . We remark that this notion can be reformulated as a standard reasoning problem, that is, C is implicitly concept-definable from Θ under O iff

where OΘ and CΘ are obtained from O and C, respectively, by uniformly replacing every concept name A ̸∈ Θ by a fresh concept name. We define C to be explicitly concept-definable fromΘ under O iff there exists a complex concept D (called an explicit concept-definition) such that O ⊨ C ≡ D and con(D) ⊆ Θ.

Definition 2 (Concept-Based Beth Definability). Let L be a DL, C be a complex concept in L, O be an L-ontology, and Θ ⊆ con(C,O). We say that L has the concept-name Beth definability property (CBP) iff if C is implicitly conceptdefinable from Θ under O, then C is explicitly conceptdefinable from Θ under O.

It is typical to establish definability properties by means of an interpolation theroem (cf. [ten Cate et al., 2013; Craig, 1957; Jung et al., 2022]). We therefore define a suitable notion of interpolation that implies the CBP, which we call concept interpolation.

Definition 3 (Concept Interpolation Property). Let L be a DL, O1 and O2 be L-ontologies with O = O1 ∪ O2, and C and D be L-concepts. We define an L-concept I to be a concept interpolant for C ⊑ D under O iff (1) con(I) ⊆ con(O1, C) ∩ con(O2, D), (2) O ⊨ C ⊑ I, and (3) O ⊨ I ⊑ D. A DL L enjoys the concept interpolation property if for all L-ontologies O1, O2 with O = O1 ∪ O2 and L-concepts C, D such that O ⊨ C ⊑ D there exists a concept interpolant for C ⊑ D under O.

Lemma 1. If a DL L enjoys the concept interpolation property, then it enjoys the CBP.

2.3 R-Systems

We let R serve as our alphabet with each role serving as a character. The set R∗ of strings over R is defined to be the smallest set satisfying the following conditions: (i) R∪{ε} ⊆ R∗ with ε the empty string, and (ii) If S ∈ R∗ and r ∈ R, then Sr ∈ R∗ , where Sr represents the concatenation of S and r. We use S,R, . . . (potentially annotated) to denote strings from R∗ , and we have Sε = εS = S, for the empty string ε. The inverse operation on strings is defined as: (1) Inv(ε) := ε, and (2) If S = r1 · · · rn, then Inv(S) := Inv(rn) · · · Inv(r1).

We now define R-systems, which are special types of SemiThue systems [Post, 1947], relative to ontologies. These will permit us to derive strings of roles from a given role and encode the information present in a given ontology.

2 In this paper, we take a DL L to be RIQ or a fragment thereof.

Definition 4 (R-system). Let O be an ontology. We define the R-systemG(O) to be the smallest set of production rules of the form r -→ S, where r ∈ R and S ∈ R∗ , such that if r1 ◦ · · · ◦ rn ⊑ s ∈ O, then

Definition 5 (Derivation, Language). Let O be an ontology and G(O) be its R-system. We write S -→G(O) R and say that the string R may be derived from the string S in one-step iff there are strings S′ ,R′ ∈ R∗ and r -→ T ∈ G(O) such that S = S′ rR′ and R = S′TR′ . We define the derivation relation -→∗G(O) to be the reflexive and transitive closure of -→G(O). For S, R ∈ R∗ , we call S -→∗G(O) R a derivation of R from S, and define the length of a derivation to be the minimal number of one-step derivations required to derive R from S in G(O). Last, we define the language LG(O)(r) := {S | r -→∗G(O) S}, where r ∈ R.

3 Sequent Systems

We let Lab = {x, y, z, . . .} be a countably infinite set of labels, define a role atom to be an expression of the form r(x, y) with r ∈ R and x, y ∈ Lab, define an equality atom and inequality atom to be an expression of the form x ˙= y and x ̸ ˙= y with x, y ∈ Lab, respectively, and define a labeled concept to be an expression x : C with x ∈ Lab and C a complex concept. We refer to role, equality, and inequality atoms as structural atoms more generally. For a (multi)set X and Y of structural atoms and/or labeled concepts, we let X, Y represent their union and let Lab(X) be the set of labels occurring therein. We say that a set Γ of structural atoms forms a tree iff the graph T (Γ) = (V, E) is a directed tree with V = Lab(Γ), and (x, y) ∈ E iff r(x, y) ∈ Γ. A sequent is defined to be an expression of the form S := Γ ⊢ ∆ such that (1) Γ is a set of structural atoms that forms a tree, (2) ∆ is a multiset of labeled concepts, (3) if Γ ̸= ∅, then Lab(∆) ⊆ Lab(Γ), and (4) if Γ = ∅, then |Lab(∆)| = 1. In a sequent Γ ⊢ ∆, we refer to Γ as the antecedent, ∆ as the consequent, and we define ∆↾x := {C | x : C ∈ ∆}.

Recall that every GCI in an ontology O is assumed to be of the form ⊤ ⊑ C. For an ontology O = R ∪ T and label x ∈ Lab, we let x : ˙¬TO = x : ˙¬C1, . . . , x : ˙¬Cn such that T = {⊤ ⊑ C1, . . . , ⊤ ⊑ Cn}. For labels x1, . . . , xn ∈ Lab, we define Γ̸ ˙=(x1, . . . , xn) = {xi ̸ ˙=xj | 1 ≤ i < j ≤ n}. We let x ≈ y ∈ {x ˙=y, y ˙=x} and write x =∗Γ y iff there exist z1, . . . , zn ∈ Lab(Γ) such that z1 ≈ z2, . . . , zn-1 ≈ zn with x = z1 and y = zn. We make use of equivalence classes of labels in the formulation of certain inference rules below and define [x]Γ := {y | x =∗Γ y} for a sequent Γ ⊢ ∆.

A uniform presentation of our sequent systems in presented in Figure 1. We note that each sequent calculus S(O) takes a RIQ-ontology O as an input parameter, which determines the functionality of certain inference rules depending on the contents of O. The calculus S(O) contains the initial rules (id) and (id ˙=), which generate axioms that are used to begin a proof, the logical rules (⊔), (⊓), (∃r), (∀r), (⩽nr), and (⩾nr), which introduce complex concepts, and the substitution rule (s ˙=). We note that A ∈ NC in the (id) rule and L is a literal in the (s ˙=) rule.

The (id ˙=) and (s ˙=) rules are subject to a side condition, namely, each rule is applicable only if x =∗Γ y. The (∀r) and (⩽nr) rules are subject to side conditions as well: the label y and the labels y0, . . . , yn must be fresh in (∀r) and (⩽nr), respectively, meaning such labels may not occur in the conclusion of a rule application. Last, we note that the (∃r) and (⩾nr) rules are special types of logical rules, referred to as propagation rules; cf. [Castilho et al., 1997; Fitting, 1972]. These rules operate by viewing sequents as types of automata, referred to as propagation graphs, which bottom-up propagate formulae along special paths, referred to as propagation paths (see Example 1 below).

Definition 6 (Propagation Graph). We define the propagation graph PG(Γ) = (V, E) of a sequent Γ ⊢ ∆ such that [x]Γ ∈ V iff x ∈ Lab(Γ), and ([x]Γ, r, [y]Γ), ([y]Γ, Inv(r), [x]Γ) ∈ E iff there exist z ∈ [x]Γ and w ∈ [y]Γ such that r(z,w) ∈ Γ. If we write [x]Γ ∈ PG(Γ), then we mean [x]Γ ∈ V , and if we write ([x]Γ, r, [y]Γ) ∈ PG(Γ), we mean ([x]Γ, r, [y]Γ) ∈ E.

We note that our propagation graphs are generalizations of those employed in sequent systems for modal and nonclassical logics [Ciabattoni et al., 2021; Gor´e et al., 2011; Lyon, 2021]. In particular, due to the inclusion of equality atoms, we must define propagation graphs over equivalence classes of labels, rather than over labels themselves. This lets us define novel and correct propagation rules in the presence of (in)equalities and counting quantifiers.

Definition 7 (Propagation Path). Given a propagation graph PG(Γ) = (V,E), [x]Γ, [y]Γ ∈ V , and r ∈ R, we write PG(Γ) ⊨ [x]Γ r⇝ [y]Γ iff ([x]Γ, r, [y]Γ) ∈ E. Given a string rS ∈ R∗ where r ∈ R, we define PG(Γ) ⊨ [x]Γ rS⇝ [y]Γ as '∃[z]Γ∈V PG(Γ) ⊨ [x]Γ r⇝ [z]Γ and PG(Γ) ⊨ [z]Γ S⇝ [y]Γ', and we take PG(Γ) ⊨ [x]Γ ε⇝ [y]Γ to mean that [x]Γ = [y]Γ. Additionally, when PG(Γ) is clear from the context we may simply write [x]Γ S⇝ [y]Γ to express PG(Γ) ⊨ [x]Γ S⇝ [y]Γ. Finally, given a language LG(O)(r) of some R-system G(O) and r ∈ R, we use [x]Γ L⇝ [y]Γ with L = LG(O)(r) iff there is a string S ∈ LG(O)(r) such that [x]Γ S⇝ [y]Γ.

To provide intuition concerning the functionality of propagation rules, we illustrate a (bottom-up) application of (⩾nr). Example 1. Let us consider the sequent Γ ⊢ x : ⩾2r.C with Γ = r(x, y), r(x, z), r(x,w), z ˙=w. A pictorial representation of the propagation graph PG(Γ) is shown below.

One can see that there are two labels y and z such that [x]Γ r⇝ [y]Γ and [x]Γ r⇝ [z]Γ. Note that r ∈ LG(O)(r) by definition. Therefore, we may (bottom-up) apply the (⩾nr) rule to obtain the three premises Γ ⊢ x : ⩾2r.C, y : C, Γ ⊢ x : ⩾2r.C, z : C, and Γ, y ˙=z ⊢ x : ⩾2r.C.

We define a proof in S(O) inductively: (1) each instance of an initial rule (r), as shown below left, is a proof with conclusion S, and (2) if n proofs exist with the respective

Side Conditions:

†3 = 'y is fresh.'

Figure 1: The calculus S(O) for the RIQ-ontology O. The rules with side conditions †1 - †5 are applicable only if that side condition holds.

conclusions S1, . . ., Sn, then applying an n-ary rule (r′ ), as shown below right, yields a new proof with conclusion S.

We use π (potentially annotated) to denote proofs, and we say a sequent S is provable with π in S(O), written S(O), π ⊩ S iff S is the conclusion of π. We write S(O) ⊩ S to indicate that S is provable with some π in S(O). Observe that each proof is a tree of sequents with the conclusion as the root. We define the height of a proof to be the number of sequents along a maximal branch from the conclusion to an initial rule of the proof. The size of a proof π is defined to be the sum of the weights of the sequents it contains; in other words, s(π) := ∑S∈π w(S), where the weight of a sequent S = Γ ⊢ ∆ is defined to be w(S) := |Γ| + ∑x:C∈∆ w(C). Ignoring labeled concepts of the form x : ˙¬TO, we refer to the formulae that are explicitly mentioned in the premises of a rule as active, and those explicitly mentioned in the conclusion as principal. For example, r(x, y) and y : C are active in (∀r) while x : ∀r.C is principal.

We now define a semantics for our sequents, which is used to establish our sequent systems sound and complete.

Definition 8 (Sequent Semantics). Let I = (∆I , ·I ) be an interpretation, S = Γ ⊢ ∆ a sequent, λ : Lab(Γ, ∆) → ∆I a label assignment, and O an ontology.

• I, λ ⊨∀ Γ iff for each r(x, y), x ˙=y, x̸ ˙=y ∈ Γ, we have (λ(x), λ(y)) ∈ rI , λ(x) = λ(y), and λ(x) ̸= λ(y);
• I, λ ⊨∃ ∆ iff for some x : C ∈ ∆, λ(x) ∈ C I .

A sequent S = Γ ⊢ ∆ is satisfied in I with λ relative to O, written I, λ ⊨O S, iff if I ⊨ O and I, λ ⊨∀ Γ, then I, λ ⊨∃ ∆. A sequent S = Γ ⊢ ∆ is true in I relative to O, written I ⊨O S, iff I, λ ⊨O S for all label assignments λ. A sequent S = Γ ⊢ ∆ is valid relative to O, written ⊨O S, iff I ⊨O S for all interpretations I, and we say that S is invalid relative to O otherwise, writing ̸⊨O S.

Lemma 2. Let I = (∆I , ·I ) be an interpretation, O be a RIQ ontology, λ be a label assignment, and Γ be a set of structural atoms. If I ⊨ O, I, λ ⊨∀ Γ, and PG(Γ) ⊨ [x]Γ L⇝ [y]Γ with L = LG(O)(r), then (λ(x), λ(y)) ∈ rI .

Theorem 1 (Soundness). If S(O) ⊩ Γ ⊢ ∆, then ⊨O Γ ⊢ ∆.

We now confirm that S(O) enjoys desirable proof-theoretic properties, viz. certain rules are height-preserving admissible or invertible. A rule is (height-preserving) admissible, i.e. (hp-)admissible, if the premises of the rule have proofs (of heights h1, . . . , hn), then the conclusion of the rule has a proof (of height h ≤ max{h1, . . . , hn}). If we let (r-1 ) be the inverse of the rule (r) whose premise is the conclusion of (r) and conclusion is the premises of (r), then we say that (r) is (height-preserving) invertible, i.e. (hp-)invertible iff (r-1 ) is (hp-)admissible. For a sequent S = Γ ⊢ ∆, we let S(x/y) = Γ(x/y) ⊢ ∆(x/y) denote the sequent obtained by substituting each occurrence of the label y in S by x; for example, if S = r(x, y), x ̸= y ⊢ y : A, then S(z/y) = r(x, z), x ̸= z ⊢ z : A. Important (hp-)admissible rules are displayed in Figure 2.

Lemma 3. The (⊤) rule is provable in S(O), and the (ℓxy ), (w ˙= ), (w̸ ˙= ), (w), (c), and (s ̸ ˙= ) rules are hp-admissible.

Lemma 4. All non-initial rules in S(O) are hp-invertible.

The completeness of S(O) (stated below) is shown by taking a sequent of the form ∅ ⊢ x : ˙¬TO, x : C as input and showing that if the sequent is not provable, then S(O) can be used to construct a counter-model thereof, witnessing the invalidity of the sequent relative to O.

The following corollary is a consequence of Theorem 1 and Theorem 2. We write S(O) ⊩ C ⊑ D as shorthand for S(O) ⊩ ∅ ⊢ x : ˙¬TO, x : ˙¬C ⊔D.

Last, we emphasize the modularity of our sequent systems and approach. By omitting inference rules for certain connectives and/or only accepting certain ontologies as the input parameter O, sequent calculi can be obtained for expressive and lightweight DLs serving as fragments of RIQ; cf. [Baader et al., 2005; Calvanese and De Giacomo, 2003]. For example, sequent calculi for ALC ontologies are easily obtained by

Figure 2: (Hp-)admissible rules in S(O). The side conditions are: †1 = 'x is fresh,' †2 = 'x, y ∈ Lab(Γ,∆),' and †3 = 'x ∈ Lab(Γ,∆).'

omitting the (id ˙=), (s ˙=), (⩾nr), and (⩽nr) rules. The constructive method presented next applies to fragments of RIQ by leveraging this feature, thus demonstrating its generality.

4 Constructive Sequent-BasedMethod

We now describe our methodology for computing concept interpolants, and by extension, explicit concept-definitions of implicitly defined concepts (by Lemma 1). The central idea is to generalize the notion of a concept interpolant from GCIs to sequents. Then, given a proof of a sequent S, we assign concept interpolants to all initial sequents of the proof, and show how a concept interpolant can be defined for the conclusion of a rule application from those of its premises, culminating in a concept interpolant for S. As sequents are more general than GCIs, this approach will establish, in a constructive manner, that RIQ (and its various sublogics) enjoy the concept interpolation property and the CBP.

Definition 9 (Interpolant). We define an interpolant to be a set G := {Γi ⊢ ∆i | 1 ≤ i ≤ n} such that Γi is a set of (in)equalities of the form x ˙=y and x̸ ˙=y with x, y ∈ Lab distinct labels, and ∆i is a set of labeled concepts. Given an interpolant G of the above form, we define its orthogonal G as follows: Γ ⊢ ∆ ∈ G iff for each 1 ≤ i ≤ |Γ, ∆|, one and only one of the following holds: (1) x ˙=y ∈ Γ with x̸ ˙=y ∈ Γi, (2) x ̸ ˙=y ∈ Γ with x ˙=y ∈ Γi, or (3) x : ˙¬C ∈ ∆ with x : C ∈ ∆i. We use G and annotated versions for interpolants.

Example 2. Let G = {(x ˙=y ⊢ x : A), (z ̸ ˙=u ⊢ z : ¬B)}. Then, the orthogonal G is the set containing (x ̸ ˙=y, z ˙=u ⊢ ), (x ̸ ˙=y ⊢ z : B), (z ˙=u ⊢ x : ¬A), and ( ⊢ x : ¬A, z : B), that is, each member of G is formed by including a negated element from each member of G.

In order to fully specify our interpolant construction algorithm, we need to define two special interpolants, named ∀r.G and ⩽nr.G, which appear in quantifier and qualified number restriction rules. We let #» C denote a set of complex concepts, define x : #» C := {x : C | C ∈ #» C}, and define � #» C, ⊔ #» C, and ˙¬ #» C to be the conjunction, disjunction, and negation of all complex concepts in #» C, respectively.

Definition 10. Let G = {Γ ⊢ ∆i, y : #» Ci | 1 ≤ i ≤ m} such that y ̸∈ Lab(Γ) and ∆i↾y = ∅, then we define:

Let G = {Γ, Γ′ ⊢ ∆i, y0 : #» C0,i, . . . , yn : #» Cn,i | 1 ≤ i ≤ m} such that Lab(Γ) ∩ {y0, . . . , yn} = ∅, Γ′ ⊆ Γ̸ ˙=(y0, . . . , yn), ∆i↾yj = ∅ for 0 ≤ j ≤ n, and #» Ci = #» C0,i, . . . , #» Cn,i. Then,

An interpolation sequent is defined to be an expression of the form Γ;Φ a |b Ψ ⊢ ∆ a |b Σ ∥ G such that Γ is a set of role and equality atoms, Φ,Ψ is a set of inequality atoms, ∆,Σ is a multiset of labeled concepts, G is an interpolant, and a, b ∈ {1, 2} with a ̸= b. For an interpolation sequent of the aforementioned form, we refer to Γ,Φ ⊢ ∆ as the left partition and Γ,Ψ ⊢ Σ as the right partition. Recall that for a concept interpolant I of a GCI C ⊑ D under O, the ontology O is the union of two ontologies O1 and O2 such that con(I) ⊆ con(O1, C) ∩ con(O2, D) (see Definition 3). The use of a, b ∈ {1, 2} in an interpolation sequent is to keep track of which partition is associated with which ontology, e.g. in Γ;Φ 1 |2 Ψ ⊢ ∆ 1 |2 Σ ∥ G the left (right) partition is associated with O1 (O2, respectively).

Definition 11 (Interpolant Preserving Rules). Let (r) be a rule in the set {(s ˙=), (⊔), (⊓), (∃r), (⩾nr)} of the form shown below and assume that the active equalities and/or labeled concepts occur in Γi and/or Σi, respectively, with the principal formula in Σ.

We define its corresponding interpolant rule as follows:

We refer to a rule (sI˙=), (⊔I ), (⊓I ), (∃rI ), or (⩾nrI ) as an interpolant preserving rule, or IP-rule. We stipulate that (∃rI ) and (⩾nrI ) are subject to the same side conditions as (∃r) and (⩾nr), respectively, w.r.t. the propagation graph PG(Γ).

For each sequent calculus S(O), we define its corresponding interpolation calculus accordingly:

Observe that interpolation calculi contain IP-rules as well as rules from Figure 3. In an interpolation calculus SI(O), the (idI1 ), (idI2 ), and (idI˙=) rules are the initial rules, (O) is the orthogonal rule, (sI˙=) is the substitution rule, and all remaining rules are logical rules. The orthogonal rule cuts the number of rules needed in SI(O) roughly in half as it essentially 'swaps' the left and right partition permitting rules to be defined that only operate within the right partition; cf. [Lyon et al., 2020]. A proof, its height, and the provability relation ⊩ are defined in SI(O) in the same manner as for S(O).

We now put forth a sequence of lemmas culminating in the main interpolation theorem (Theorem 3), which implies that RIQ has the CBP (Corollary 2). We remark that Lemmas 5 and 7 describe proof transformation algorithms between S(O) and SI(O). In particular, Lemma 5 states that

Figure 3: Rules in SI(O). The (idI˙=), (∀rI ), and (⩽nrI ) rules satisfy the same side conditions as (id ˙=), (∀r), and (⩽nr), respectively.

each proof in S(O) of a sequent Γ,Φ,Ψ ⊢ ∆,Σ in a special form can be transformed into a proof in SI(O) of a specific interpolation sequent Γ;Φ a |b Ψ ⊢ ∆ a |b Σ ∥ G. Then, via Lemma 7, this proof can be transformed into two proofs in S(O) witnessing that the interpolant G is 'implied by' the left partition Γ,Φ ⊢ ∆ and 'implies' the right partition Γ,Ψ ⊢ Σ. Both Lemmas 5 and 7 are shown by induction on the height of the given proof. Last, when we use the notation Γ,Φa,Φb ⊢ ˙¬TOa ,∆a,∆b, ˙¬TOb or the notation Γ;Φa a |b Φb ⊢ ˙¬TOa ,∆a a |b ∆b, ˙¬TOb ∥ G, we assume that ˙¬TOc := x1 : ˙¬TOc , . . . , xn : ˙¬TOc such that Lab(Γ, Φc,∆c) = {x1, . . . , xn} and c ∈ {a, b}. The use of ˙¬TOc ensures each partition satisfies its respective ontology.

Lemma 5. Let O = O1 ∪ O2 be an ontology and suppose that Γ,Φ,Ψ ⊢ ˙¬TOa ,∆,Σ, ˙¬TOb has a proof π in S(O) with Φ∩Ψ = ∅. Then, π can be transformed into a proof in SI(O) of Γ;Φ a |b Ψ ⊢ ˙¬TOa ,∆ a |b Σ, ˙¬TOb ∥ G such that:

1. If x ˙=y occurs in G, then x̸ ˙=y ∈ Φ;
2. If x̸ ˙=y occurs in G, then x̸ ˙=y ∈ Ψ;

1. con(G) ⊆ con(Oa,∆) ∩ con(Σ,Ob).

The following lemma states that a double orthogonal transformation always 'preserves' some of the sequents from the original interpolant. As proven in the appended version [Lyon and Karge, 2024], the lemma is helpful in showing Lemma 7.

1. For each (Γ′ ⊢ Πi) ∈ G, S(O) ⊩ Γ, Γ′ , Φ ⊢ ∆, Πi;

Next, we prove that an interpolant containing at most a single label, i.e. an interpolant of the form

can be transformed into a single labeled concept within the context of a proof. Toward this end, we define x : �⊔ G := x : �1≤i≤n ⊔1≤j≤ki Ci,j, where G is as above. The following two lemmas are straightforward and follow by applying the (⊔) and (⊓) rules in S(O) a sufficient number of times.

Our main theorem below is a consequence of Lemmas 4-9. Given a proof of ⊢ x : ˙¬TO, x : ˙¬C⊔D, we obtain proofs of ⊢ x : ˙¬TO1 , x : ˙¬C, x : I and ⊢ x : ˙¬TO2 , x : D, x : ˙¬I in S(O) by Lemmas 4, 5, and 7-9 with I = �⊔ G. The concept interpolant I is computed in EXPTIME due to the potential use of the (O) rule, which may exponentially increase the size of interpolants.

Theorem 3. Let O = O1 ∪O2 be a RIQ ontology. If O ⊨ C ⊑ D, i.e. S(O), π ⊩ C ⊑ D, then a concept interpolant I can be computed in EXPTIME relative to s(π) such that S(O) ⊩ C ⊑ I and S(O) ⊩ I ⊑ D, i.e. O ⊨ C ⊑ I and O ⊨ I ⊑ D.

Let C be a complex concept, O be a RIQ ontology, Θ ⊆ con(C,O), and suppose C is implicitly concept-definable from Θ under O. If we want to find the explicit conceptdefinition of C from Θ under O, we utilize the sequent calculus S(O′ ) with O′ = O ∪OΘ. Since C is implicitly conceptdefinable, we know by (1) in Section 2.2 and Corollary 1 that S(O′ ) ⊩ C ⊑ CΘ. By applying Theorem 3, we obtain a concept interpolant I for C ⊑ CΘ under O, which serves as an explicit concept-definition by Lemma 1. Therefore, we have a constructive proof of the following corollary.

Corollary 2. RIQ has the concept interpolation property and the CBP.

5 Concluding Remarks

There are various avenues of future research. First, it would be interesting to know the size and complexity of computing a concept interpolant I relative to C ⊑ D rather than from a proof π witnessing O ⊨ C ⊑ D. This can be achieved by supplying a proof-search algorithm that generates a proof of C ⊑ D, whose relative complexity and size can then be determined. Second, we aim to generalize our methodology to decide and compute the existence of Craig interpolants for RIQ and related DLs, which is a non-trivial problem (see [ten Cate et al., 2013]). Last, we could generalize our method to consider constructs beyond those in RIQ, e.g. negations over roles, intersections of roles, nominals, or the @ operator; it is known that for some of these extensions, e.g. nominals, even concept interpolation fails [Artale et al., 2023], requiring an increase in complexity to decide the existence of interpolants.

Acknowledgments

Tim S. Lyon is supported by the European Research Council (ERC) Consolidator Grant 771779 (DeciGUT). Jonas Karge is supported by BMBF (Federal Ministry of Education and Research) in DAAD project 57616814 (SECAI, School of Embedded Composite AI) as well as by BMBF in the Center for Scalable Data Analytics and Artificial Intelligence (ScaDS.AI).