Constructive Interpolation and Concept-Based Beth Definability for Description Logics via Sequents
Tim S. Lyon Jonas Karge


 
      Extending Cislunar Communication Network Reach Using Reconfigurable Intelligent Surfaces
     Aamer Mohamed Huroon*§,
    Baris Donmez§,
    Yu-Chih Huang†,
     Gunes Karabulut Kurt§,
   and Li-Chun Wang‡
   

* 
            EECS International Graduate Program, National Yang Ming Chiao Tung University  

    † 
            Institute of Communications Engineering, National Yang Ming Chiao Tung University

         ‡ Department of Electrical and Computer Engineering, National Yang Ming Chiao Tung University 

       § 
           Dept. of Electrical Engineering, Polytechnique Montréal, Montréal, Canada

       E-mail: *†‡{aamer.ee08, jerryhuang, wang}@nycu.edu.tw §{aamer.mohamed-huroon-mohamed, baris.donmez, gunes.kurt}@polymtl.ca 
    April 29, 2024
===========================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================




We introduce a constructive method applicable to a large number of description logics (DLs) for establishing the concept-based Beth definability property (CBP) based on sequent systems. Using the highly expressive DL  as a case study, we introduce novel sequent calculi for -ontologies and show how certain interpolants can be computed from sequent calculus proofs, which permit the extraction of explicit definitions of implicitly definable concepts. To the best of our knowledge, this is the first sequent-based approach to computing interpolants and definitions within the context of DLs, as well as the first proof that  enjoys the CBP. Moreover, due to the modularity of our sequent systems, our results hold for any restriction of , and are applicable to other DLs by suitable modifications.





§ 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 𝖭𝖾𝗐𝖢 can be defined in one of two ways: (1) implicitly, by specifying a set of axioms such that the interpretation of 𝖭𝖾𝗐𝖢 is uniquely determined by the interpretation of the given concepts and relations, or (2) explicitly, by writing a definition 𝖭𝖾𝗐𝖢≡𝖣 where 𝖭𝖾𝗐𝖢 does not appear in 𝖣. Description logics for which implicit definability implies explicit definability are said to be definitorially complete <cit.>, or to exhibit the concept-based Beth definability property (CBP) <cit.>. This is Beth's definability property <cit.> 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 <cit.>. This is of particular importance since reasoning with acyclic terminologies is usually less complex than with general ones, e.g. satisfiability over acyclic -terminologies is -complete while being -complete over general -terminologies <cit.>. 
Other applications include, rewriting ontology-mediated queries <cit.>, learning concepts separating positive and negative examples <cit.>, and computing referring expressions, which is of value in computational linguistics and data management <cit.>. 


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 , , and  <cit.>. 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 <cit.> or which compute explicit definitions using tableau-based algorithms <cit.>. 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 <cit.>. 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 <cit.> and being used to establish non-trivial properties of logics such as consistency <cit.>, decidability <cit.>, and interpolation <cit.>. Regarding this last point, it was first shown by Maehara that sequent systems could be leveraged to constructively prove the Craig interpolation property <cit.> 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 <cit.>, intermediate logics <cit.>, and temporal logics <cit.>. 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 -ontologies 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 <cit.>, 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 -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. <cit.>. 

Finally, we remark that although our work shares similarities with that of <cit.>, our method goes beyond this work as we establish the CBP for the highly expressive DL , and due to the modularity of our sequent systems, our method is applicable to any restriction of , e.g. logics within the  and  families <cit.>. 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 . Our work also intersects that of <cit.>, which establishes the CBP for  extended with PUR Horn conditions, but differs both in terms of methodology and our consideration of qualified number restrictions.


Outline of Paper: In Section <ref>, we define the 
logic , define the CBP and related notions, and explicate certain grammar theoretic concepts used in formulating inference rules. In Section <ref>, we present our sequent systems and establish that each system enjoys fundamental 
properties. Section <ref> develops and explains our new sequent-based method that computes explicit definitions of implicitly definable concepts and establishes the CBP, using  as case study. To the best of our knowledge, this is the first proof that  has the CBP. In Section <ref>, we conclude and discuss future work. We note that all proofs have been deferred to the appendix.

























§ PRELIMINARIES




In the first part of this section, we introduce the language and semantics for the description logic , which subsumes various expressive and lightweight DLs
 <cit.>. 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 <cit.>, referred to as -systems, which are essential in the formulation of our sequent calculi. 



 §.§ Language and Semantics: 


The description logic  is defined relative to a vocabulary = (, ), which is a pair containing pairwise disjoint, countable sets. The set  contains role names used to denote binary relations and the set  contains concept names used to denote classes of entities. We use the (potentially annotated) symbols , , … to denote role names, and A, B, … to denote concept names. We define a role to be a role name or an inverse role  such that ∈. We define the inverse of a role to be = and = given that ∈. We let := ∪{ |  ∈} denote the set of roles.

 A complex role inclusion axiom (RIA) is an expression _1∘⋯∘_n such that _1, …, _n and  are roles, and ∘ denotes the usual composition operation over binary relations; we assume n-ary compositions _1∘⋯∘_n associate to the left. We define an RBox  to be a finite collection of RIAs. As identified by Horrocks and Sattler <cit.>, to ensure the decidability of reasoning with , only regular RBoxes may be used in ontologies (defined below).[Note, our interpolation results go through for general RBoxes, i.e. this restriction is not needed for the work in Sections <ref> and <ref>.] 
  Let ≺ be a strict partial order on the set  of role names; we define an RIA w to be ≺-regular  is a role name, and either (1) w =, (2) w = ^-, (3) w = _1 ∘⋯∘_n and _i ≺ for all 1 ≤ i ≤ n, (4) w = ∘_1 ∘⋯∘_n and _i ≺ for all 1 ≤ i ≤ n, or (5) w = _1 ∘⋯∘_n ∘ and _i ≺ for all 1 ≤ i ≤ n. An RBox  is defined to be regular a strict partial order ≺ over  exists such that every RIA in  is ≺-regular. 
 
We recursively define a role name  to be simple (with respect to an RBox ) either (1) no RIA of the form w occurs in , or (2) for each ∈,  is a simple role name or its inverse is. Also, an inverse role  is defined to be simple if  is simple.
 


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

    C ::= A  |   A  |  (C ⊙ C)  |  (Q . C)  |  (⩽ n .C)  |  (⩾ n .C)

where A ∈, ⊙∈{, }, Q ∈{∃, ∀ |  ∈},  is a simple role, and n ∈ℕ. We use the symbols C, D, … (potentially annotated) to denote complex concepts. We define ⊤ = A  A and = A  A for a fixed A ∈, and define a literal L to be either a concept name or its negation, i.e. L ∈{A,  A  |  A ∈}. 
 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 
 (⩽ n .C) := (⩾ (n+1) . C), and 

    (⩾ n . C) :=
         if n=0,
    ⩽ (n-1) . C    otherwise.


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




  ∙ L = 1 with L ∈{A,  A  |  A ∈};


  ∙ C ⊙ D = C + D + 1 with ⊙∈{, };


  ∙ Q.C = C + 1 with Q ∈{∃, ∀ |  ∈};


  ∙ ⩽ n .C = C + n + 1;


  ∙  ⩾ n .C = 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  is a finite set of GCIs and we make the simplifying assumption that every GCI in a TBox  is of the form ⊤⊑ C.  We define a -ontology  (which we refer to as an ontology for short) to be the union of an RBox  and TBox , that is, = ∪. For a set X of concepts, GCIs, or RIAs, we let X denote the set of all concept names occurring in X, and we let X denote the set of all concept names and roles occurring in X. Symbols from a vocabulary  are interpreted accordingly:
 
 




 An interpretation = (,·) is a pair consisting of a non-empty set  called the domain and a map · such that





  ∙ if A ∈, then A⊆ with A = ∖A;


  ∙ if ∈, then ⊆×.


 We define () = {(b,a)  |  (a,b) ∈} and interpret compositions over roles in the usual way. 




 
We lift interpretations to complex concepts accordingly: 



  ∙ (C ⊔ D) = C∪D;


  ∙ (C ⊓ D) = C∩D;


  ∙ ∃. C = {a ∈ |  ∃ b ∈,  (a,b) ∈ & b ∈C};


  ∙ ∀. C = {a ∈ |  ∀ b ∈, (a,b) ∈⇒ b ∈C};


  ∙ C:={a ∈ :  {b  :  (a,b) ∈ & b ∈C}≤ n };


  ∙ C:={a ∈ :  {b  :  (a,b) ∈ & b ∈C}≥ n }.


An interpretation satisfies C  D or _1∘⋯∘_n, written C ⊑ D and _1∘⋯∘_n C⊆D and (_1∘⋯∘_n)⊆, respectively. An interpretation  is defined to be a model of an ontology , written , it satisfies all GCIs and RIAs in . We write C  D for every interpretation , if , then C  D, and we write C ≡ D when C ⊑ D and D ⊑ C.







 §.§ Definability and Interpolation





The notion of 
Beth definability, first defined within the context of first-order logic <cit.>, takes on a number of distinct formulations within the context of DLs. In <cit.>, Beth definability is reinterpreted as the notion of definitorial completeness, which has also been named concept-based Beth definability (CBP) <cit.>. Intuitively, a DL  has the CBP when the implicit definability of a concept C under an -ontology  using a signature = ∪ with ⊆C, 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 ⊆C,, or the weaker Beth definability property (BDP) where the signature  is the set of all symbols distinct from the concept defined <cit.>. In this paper, we focus on the CBP, and leave the investigation of sequent-based methodologies for establishing other definability properties to future work. Let us now formally define the CBP.



Let  be a DL, C be a complex concept in ,  an -ontology, and ⊆C,.[In this paper, we take a DL  to be  or a fragment thereof.] We define C to be implicitly concept-definable from  under  for any two models  and  of  such that = and for each P ∈∪, P^ = P^, it follows that C^ = C^. We remark that this notion can be reformulated as a standard reasoning problem, that is, C is implicitly concept-definable from  under  
    ∪_ C  C_

where _ and C_ are obtained from  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  there exists a complex concept D (called an explicit concept-definition) such that C ≡ D and D⊆.

 Let  be a DL, C be a complex concept in ,  be an -ontology, and ⊆C,. We say that  has the concept-name Beth definability property (CBP) if C is implicitly concept-definable from  under , then C is explicitly concept-definable from  under . 


It is typical to establish definability properties by means of an interpolation theroem (cf. <cit.>). We therefore define a suitable notion of interpolation that implies the CBP, which we call concept interpolation.


 Let  be a DL, _1 and _2 be ℒ-ontologies with = _1∪_2, and C and D be ℒ-concepts. We define an ℒ-concept I to be a concept interpolant for C  D under  (1) I⊆_1, C∩_2, D, (2) C  I, and (3) I  D. A DL ℒ enjoys the concept interpolation property if for all ℒ-ontologies _1, _2 with = _1∪_2 and ℒ-concepts C, D such that C ⊑ D there exists a concept interpolant for C ⊑ D under .


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






 §.§ -Systems


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


We now define -systems, which are special types of Semi-Thue systems <cit.>, 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. 

 Let  be an ontology. We define the -system  to be the smallest set of production rules of the form , where ∈ and ∈, such that if _1∘⋯∘_n∈, then

    (_1⋯_n), (_n⋯_1) ∈.











 Let  be an ontology and  be its -system. We write _ and say that the string  may be derived from the string  in one-step there are strings ', ' ∈ and ∈ such that = ' ' and = ' '. We define the derivation relation  to be the reflexive and transitive closure of _. For , ∈, we call  a derivation of  from , and define the length of a derivation to be the minimal number of one-step derivations required to derive  from  in . Last, we define the language () := { |  }, where ∈.































§ SEQUENT SYSTEMS




We let = {, , , …} be a countably infinite set of labels, define a role atom to be an expression of the form (,) with ∈ and , ∈, define an equality atom and inequality atom to be an expression of the form  and  with , ∈, respectively, and define a labeled concept to be an expression : C with ∈ 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 (X) be the set of labels occurring therein. We say that a set  of structural atoms forms a tree the graph T() = (V,E) is a directed tree with V = (), and (x,y) ∈ E (x,y) ∈. A sequent is defined to be an expression of the form := such that (1)  is a set of structural atoms that forms a tree, (2)  is a multiset of labeled concepts, (3) if ≠∅, then () ⊆(), and (4) if = ∅, then |()| = 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  is assumed to be of the form ⊤ C. For an ontology = ∪ and label ∈, we let :  =  : C_1, …,  : C_n such that = {⊤ C_1, …, ⊤ C_n}. For labels _1, …, _n∈, we define _1, …, _n = {_i_j |  1 ≤ i < j ≤ n}. We let x ≈ y ∈{x  y, y  x} and write xy there exist z_1, …, z_n∈() such that z_1≈ z_2, …, z_n-1≈ z_n with x = z_1 and y = z_n. We make use of equivalence classes of labels in the formulation of certain inference rules below and define x := {y  |  xy} for a sequent .





A uniform presentation of our sequent systems in presented in  <ref>. We note that each sequent calculus  takes a -ontology  as an input parameter, which determines the functionality of certain inference rules depending on the contents of . The calculus  contains the initial rules 𝕀 and , which generate axioms that are used to begin a proof, the logical rules , , , , , and , which introduce complex concepts, and the substitution rule . We note that A ∈ in the 𝕀 rule and L is a literal in the  rule. The  and  rules are subject to a side condition, namely, each rule is applicable only if xy. The  and  rules are subject to side conditions as well: the label y and the labels y_0, …, y_n must be fresh in  and , respectively, meaning such labels may not occur in the conclusion of a rule application. Last, we note that the  and  rules are special types of logical rules, referred to as propagation rules; cf. <cit.>. 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 <ref> below). 


 We define the propagation graph = (V,E) of a sequent  such that x∈ V x ∈(), and (x, , y), (y, , x) ∈ E there exist z ∈x and w ∈y such that (z, w) ∈. If we write x∈, then we mean x∈, and if we write (x,,y) ∈, we mean (x,,y) ∈.


We note that our propagation graphs are generalizations of those employed in sequent systems for modal and non-classical logics <cit.>. 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. 

 
Given a propagation graph = (V,E), x, y∈ V, and ∈, we write xy (x,,y) ∈ E. Given a string ∈ where ∈, we define xy as `∃_z∈ V xz and zy', and we take xy to mean that x = y. Additionally, when  is clear from the context we may simply write xy to express xy. Finally, given a language () of some -system  and ∈, we use xLy with L = () there is a string ∈() such that xy.


To provide intuition concerning the functionality of propagation rules, we illustrate a (bottom-up) application of . 

 Let us consider the sequent Γ x : ⩾ 2  . C with Γ = r(x,y), r(x,z), r(x,w), z  w. A pictorial representation of the propagation graph Γ is shown below.


		
[] (x) [] {y};

[] (y0) [right=of x,xshift=1cm] {x};
[] (y1) [right=of y0,xshift=1cm] {z,w};



[->, dotted](y0) to [bend right=25] node[midway,above] r (x);
[->,dotted](x) to [bend right=25] node[midway,below] r (y0);
[->,dotted](y0) to [bend left=25] node[midway,above] r (y1);
[->,dotted](y1) to [bend left=25] node[midway,below] r (y0);



One can see that there are two labels y and z such that xry and xrz. Note that r ∈() by definition. Therefore, we may (bottom-up) apply the  rule to obtain the three premises Γ x : ⩾ 2  . C, y : C, Γ x : ⩾ 2  . C, z : C, and Γ, y  z  x : ⩾ 2  . C.




We define a proof in  inductively: (1) each instance of an initial rule (r), as shown below left, is a proof with conclusion , and (2) if n proofs exist with the respective conclusions _1, …, _n, then applying an n-ary rule (r'), as shown below right, yields a new proof with conclusion .




(r)



   

_1 ⋯ _n
(r')




We use  (potentially annotated) to denote proofs, and we say a sequent  is provable with  in , written , ⊩  is the conclusion of . We write ⊩ to indicate that  is provable with some  in . 
 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, where the weight of a sequent = is defined to be := || + ∑_ : C ∈C. Ignoring labeled concepts of the form x :, 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  while x :  C is principal.





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



 Let = (,·) be an interpretation, = a sequent, : (,) → a label assignment, and  an ontology.



  ∙ , for each (,), , ∈, we have ((),()) ∈, () = (), and () ≠();


  ∙ , for some : C ∈, () ∈C.


 A sequent = is satisfied in  with  relative to , written ,, if  and ,, then ,. A sequent = is true in  relative to , written , , for all label assignments . A sequent = is valid relative to , written ,  for all interpretations , and we say that  is invalid relative to  otherwise, writing .




Let = (,·) be an interpretation,  be a  ontology, λ be a label assignment, and  be a set of structural atoms. If , ,, and xLy with L = (), then (λ(x), λ(y)) ∈.








If ⊩⊢, then . 







We now confirm that  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 h_1, …, h_n), then the conclusion of the rule has a proof (of height h ≤max{h_1, …, h_n}). 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 (r^-1) is (hp-)admissible. For a sequent =, we let (x/y) = (x/y) (x/y) denote the sequent obtained by substituting each occurrence of the label y in  by x; for example, if = r(x,y), x ≠ y  y : A, then (z/y) = r(x,z), x ≠ z  z : A. Important (hp-)admissible rules are displayed in  <ref>.






The  rule is provable in , and the xy, , , , , and  rules are hp-admissible. 




All non-initial rules in  are hp-invertible.




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



If ∅ : C, then ⊩∅ : ,  : C. 



The following corollary is a consequence of  <ref> and  <ref>. We write ⊩ C  D as shorthand for ⊩∅ x : , x : C D.




C  D ⊩ 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 , sequent calculi can be obtained for expressive and lightweight DLs serving as fragments of ; cf. <cit.>. For example, sequent calculi for  ontologies are easily obtained by omitting the , , , and  rules. 
 The constructive method presented next applies to fragments of  by leveraging this feature, 
 thus demonstrating its generality. 












§ CONSTRUCTIVE SEQUENT-BASED METHOD





We now describe our methodology for computing concept interpolants, and by extension, explicit concept-definitions of implicitly defined concepts (by  <ref>). The central idea is to generalize the notion of a concept interpolant from GCIs to sequents. Then, given a proof of a sequent , 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 . As sequents are more general than GCIs, this approach will establish, in a constructive manner, that  (and its various sublogics) enjoy the concept interpolation property and the CBP.



 We define an interpolant to be a set := {_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 ∈ distinct labels, and _i is a set of labeled concepts. Given an interpolant  of the above form, we define its orthogonal  as follows: ∈ 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  and annotated versions 
for interpolants.



 Let = {(x  y  x : A), (z  u  z :  B) }. Then, the orthogonal  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  is formed by including a negated element from each member of .


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

 Let = {_i, y : _i |  1 ≤ i ≤ m} such that y ∉() and _i y = ∅, then we define:

    := {_i,  : _i |  1 ≤ i ≤ m}.
  
Let = {, ' _i, y_0 : _0,i, …, y_n : _n,i |  1 ≤ i ≤ m} such that () ∩{y_0, …, y_n} = ∅, ' ⊆y_0, …, y_n, _i y_j = ∅ for 0 ≤ j ≤ n, and _i = _0,i, …, _n,i. Then,

    .  := { (_i,  :  .  _i)  |  1 ≤ i ≤ m}.




An interpolation sequent is defined to be an expression of the form ; ΦΨ such that  is a set of role and equality atoms, Φ, Ψ is a set of inequality atoms, , is a multiset of labeled concepts,  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 , the ontology  is the union of two ontologies _1 and _2 such that I⊆_1, C∩_2, D (see  <ref>). 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 ; ΦΨ the left (right) partition is associated with _1 (_2, respectively).





 Let  be a rule in the set {, , , , } 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 .


_i, Φ, Ψ, _i |  1 ≤ i ≤ n

, Φ, Ψ,


We define its corresponding interpolant rule as follows:




_i; ΦΨ_i_i |  1 ≤ i ≤ n

; ΦΨ_1∪⋯∪_n




We refer to a rule , , , , or  as an interpolant preserving rule, or IP-rule. We stipulate that  and  are subject to the same side conditions as  and , respectively, w.r.t. the propagation graph .



For each sequent calculus , we define its corresponding interpolation calculus accordingly:

    := {, , }∪{ |  ∈∖𝕀}

Observe that interpolation calculi contain IP-rules as well as rules from  <ref>. In an interpolation calculus , the , , and  rules are the initial rules,  is the orthogonal rule,  is the substitution rule, and all remaining rules are logical rules. The orthogonal rule cuts the number of rules needed in  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. <cit.>. A proof, its height, and the provability relation ⊩ are defined in  in the same manner as for . 

We now put forth a sequence of lemmas culminating in the main interpolation theorem ( <ref>), which implies that  has the CBP ( <ref>). We remark that Lemmas <ref> and <ref> describe proof transformation algorithms between  and . In particular, Lemma <ref> states that each proof in  of a sequent , Φ, Ψ, in a special form can be transformed into a proof  in  of a specific interpolation sequent ; ΦΨ. Then, via Lemma <ref>, this proof can be transformed into two proofs in  witnessing that the interpolant  is `implied by' the left partition , Φ and `implies' the right partition , Ψ. Both Lemmas <ref> and <ref> are shown by induction on the height of the given proof. Last, when we use the notation , Φ_a, Φ_b_a, _a, _b, _b or the notation ; Φ_aΦ_b_a, _a_b, _b, we assume that _c := x_1 : _c, …, x_n : _c such that (, Φ_c, _c) = {x_1, …, x_n} and c ∈{a,b}. The use of _c ensures each partition satisfies its respective ontology. 





Let = _1∪_2 be an ontology 
and suppose that , Φ, Ψ_a, , , _b has a proof  in  with Φ∩Ψ = ∅. Then,  can be transformed into a proof in  of ; ΦΨ_a, , _b such that:



  (1) If x  y occurs in , then x  y ∈Φ;


  (2) If x  y occurs in , then x  y ∈Ψ;


  (3) () ⊆(, Φ, Ψ, _a, , , _b); 


  (4) ⊆_a, ∩, _b.
 




The following lemma states that a double orthogonal transformation always `preserves' some of the sequents from the original interpolant. As shown in the appendix, the lemma is helpful in proving  <ref>.



If () ∈, then there exists a () ∈ such that ⊆ and ⊆. 




 



If ⊩; ΦΨ, then 



  (1) For each (' _i) ∈, ⊩, ', Φ, _i; 


  (2) For each (' _i) ∈, ⊩, ', Ψ_i,. 





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


    := {(   x : C_i,1, …, x : C_i,k_i)  |  1 ≤ i ≤ n}


can be transformed into a single labeled concept within the context of a proof. Toward this end, we define x :  :=  x: _1 ≤ i ≤ n_1 ≤ j ≤ k_i C_i,j, where  is as above. The following two lemmas are straightforward and follow by applying the  and  rules in  a sufficient number of times.



If , is provable in  for all ( ⊢) ∈ and () = {}, then ⊩,  :.





If , is provable in  for all ( ) ∈ and () = {}, then ⊩,  :. 


Our main theorem below is a consequence of Lemmas <ref>–<ref>. Given a proof of x : , x : C D, we obtain proofs of x : _1, x : C, x : I and x : _2, x : D, x : I in  by Lemmas <ref>, <ref>, and <ref>–<ref> with I =. The concept interpolant I is computed in  due to the potential use of the  rule, which may exponentially increase the size of interpolants.


Let = _1∪_2 be a  ontology. If C  D, i.e. , ⊩ C  D, then a concept interpolant I can be computed in  relative to  such that ⊩ C  I and ⊩ I  D, i.e. C  I and I  D.



Let C be a complex concept,  be a  ontology, ⊆C,, and suppose C is implicitly concept-definable from  under . If we want to find the explicit concept-definition of C from  under , we utilize the sequent calculus 𝖲(') with ' = ∪_. Since C is implicitly concept-definable, we know by (1) in Section <ref> and Corollary <ref> that 𝖲(') ⊩ C  C_. By applying Theorem <ref>, we obtain a concept interpolant I for C  C_ under , which serves as an explicit concept-definition by  <ref>. Therefore, we have a constructive proof of the following corollary.





 has the concept interpolation property and the CBP.








§ CONCLUDING REMARKS







We have provided novel sequent calculi for  ontologies, showing them sound and complete, as well as showing that each calculus enjoys useful hp-admissibility and hp-invertibility properties. Our sequent systems are modular as the omission of certain rules or constructs from ontologies yields sequent systems for restrictions of . Moreover, we presented a sequent-based methodology for computing concept interpolants and explicit definitions of implicitly definable concepts using  as a case study, thus satisfying a demand for developing constructive interpolation and definability methods. To the best of our knowledge, we have provided the first proof of the CBP for .

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 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  and related DLs, which is a non-trivial problem (see <cit.>). Last, we could  generalize our method to consider constructs beyond those in , 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 <cit.>, 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 (https://secai.org/SECAI, School of Embedded Composite AI) as well as by BMBF in the Center for Scalable Data Analytics and Artificial Intelligence (ScaDS.AI).



named








§ PROOFS FOR  <REF>




<ref> If a DL  enjoys the concept interpolation property, then it enjoys the CBP.


 Let  be an ℒ-ontology, C be an ℒ-concept, and ⊆C,. Suppose ℒ enjoys the concept interpolation property and let C be implicitly concept-definable from  under , that is, ∪_ C  C_ (see (<ref>) on p. eq:implicit-def). Then, a concept interpolant I exists such that (i) I⊆, C∩_, C_, (ii) ∪_ C  I, and (iii) ∪_ I  D. By (i) and the definitions of _ and C_, we have that I⊆. We now establish that C ≡ I. We argue that C  I, and note that the argument showing I  C is similar.

Suppose . We aim to show that C  I. First, recall that each concept name B ∈C, such that B ∉ is replaced by a fresh concept name in C_ and _, which we denote by B'. Now, let us define = (, ·^) such that Δ^ :=, for each B ∈C, such that B ∉, (B')^ := B, and for all other symbols P, let P^ := P. Observe that ∪_, meaning C  I by (ii) above. Furthermore, observe that for P ∈C, ∪, P^ = P, meaning C  I as C and I are only composed of symbols from C, ∪. It can be argued in a similar fashion that I  C, meaning, C ≡ I. 

Therefore, I serves as an explicit concept-definition of C, showing that C is explicitly concept-definable from  under , that is,  has the CBP.







§ PROOFS FOR  <REF>




<ref>
Let = (,·) be an interpretation,  be a  ontology, λ be a label assignment, and  be a set of structural atoms. If , ,, and xLy with L = (), then (λ(x), λ(y)) ∈.


 Suppose , ,, and xLy with L = (). We prove the claim by induction on the length of the derivation of the string ∈ L such that xy.

Base Case. For the base case, we suppose that the derivation of  is of length 0. By  <ref>, we know that the only derivation in () from  of length 0 is the derivation of the form , that is, the derivation consisting solely of . Therefore, xy, which implies that either (z,w) ∈ or (w, z) ∈ for z ∈x and w ∈y by  <ref>. In either case, since ,, we have that (λ(x), λ(y)) ∈.

Inductive Step. Let the derivation of  be of length n+1. By  <ref>, there is a derivation  of length n and production rule _1⋯_m∈() such that = _1⋯_m. As  is a string encoding a propagation path in , it follows that 
 _1_1_2⋯_m_m_m+1 occurs in . By  <ref>, _1(z_1',z_2'), …, _m(z_m',z_m+1') ∈ with z_i' ∈_i and

    _i+1(z_i',z_i+1') ∈{_i+1(z_i',z_i+1'), _i+1(z_i+1',z_i')}

 for 1 ≤ i ≤ m. This implies that (λ(z_1),λ(z_m+1)) ∈(s_1∘⋯∘ s_m) because ,. Furthermore, since s  s_1⋯ s_m∈(), either s_1∘⋯∘ s_m s ∈ or s_m∘⋯∘s_1s∈, by  <ref>. Regardless of the case, (λ(z_1),λ(z_m+1)) ∈s. We will use this fact to complete the proof of the inductive step below.
 
Let us consider the set ' = , (z_1',z_m+1') of relational atoms. We know that , ' because ', by assumption and (λ(z_0),λ(z_m+1)) ∈s by what was argued above. Moreover, we have that 'x'z_1'z_m+1'y'. Observe that  has a derivation of length n by what was said above. Therefore, we may invoke the induction hypothesis, from which it follows that (λ(x), λ(y)) ∈.




<ref>[Soundness]
If ⊩⊢, then . 


 By induction on the height of the proof of ⊢.


Base Case. If the height of the proof is 1, then our proof is an instance of 𝕀 or , as shown below.





: A,  :  A,


   



, x  y



We argue the 𝕀 case first, and assume for a contradiction that : A,  :  A, is invalid relative to . From this, it follows that there exists an interpretation ℐ and a label assignment λ such that ℐ, λ and ℐ, λ : A,  :  A,. Hence, λ(x) ∉ A^ℐ and λ(x) ∈ A^ℐ, which is a contradiction. For the  case, we assume for a contradiction that , x  y is invalid relative to . Then, there exists an interpretation ℐ and label assignment  such that ℐ, λ, x  y and ℐ, λ. By the side condition xy, we have that (x) = (y). However, we also have that (x) ≠(y), which is a contradiction.


Inductive Step. Assume soundness holds for proofs of height n. We now show that it holds for proofs of height n + 1. We prove each case by contraposition and argue that if the conclusion of the last inference of the proof is invalid relative to , then at least one premise of the inference must be invalid relative to .
 

The  rule:


: L,  : L,

: L,


Suppose there exists an interpretation ℐ and label assignment  such that ℐ, λ and ℐ, λ : L,. By the side condition xy imposed on , we know that (x) = (y). Since we have that () ∉L, it follows that () ∉L, which shows the premise invalid relative to .


The  rule:



: C,  : D,

: C  D,



 Assume : C  D, is invalid relative to . By  <ref>, it follows that there exists an interpretation ℐ and a label assignment λ such that ℐ, λ and ℐ, λ : C  D,. Hence, λ(x) ∉C and λ(x) ∉D. Moreover, it holds that ℐ, λ. Since ℐ, λ and ℐ, λ : C,  : D,, the premise is invalid relative to  as well.


The  rule:



: C,
: D,

: C  D,



Assume : C  D, is invalid relative to . By  <ref>, it follows that there exists an interpretation ℐ and a label assignment λ such that ℐ, λ and ℐ, λ : C  D,. Either λ(x) ∉C or λ(x) ∉D. Also, ℐ, λ. Therefore, either ℐ, λ : C, or ℐ, λ : D,, meaning, at least one of the premises must be invalid relative to  as well.


The  rule:


:  C,  : C,

:  C,


Suppose there exists an interpretation ℐ and label assignment  such that ℐ, λ and ℐ, λ :  C,. By the side condition imposed on , we know that xLy with L = (). By  <ref>, we know that (λ(x), λ(y)) ∈. As (x) ∉ C, we know that (y) ∉C, showing that the premise is invalid relative to .


The  rule:


, (,)  : C,  : ,

:  C,


Suppose, :  C, is invalid relative to . From this, it follows that there exists an interpretation ℐ and a label assignment λ such that , ℐ, λ and ℐ, λ :  C,.
Thus, there is at least one domain element a ∈ such that (λ(x),a) ∈ and a ∉C. 
We now define a new label assignment λ' such that λ'(z) = λ(z) if z ≠ y and λ'(y) = a.
Hence, ℐ, λ' , r(, ) and λ'(y) ∉C. Moreover, let y_i :  = y : D_1, … y : D_k. Since ⊤ D_j∈ for 1 ≤ j ≤ k, we have that , λ' y : as . Therefore, the premise is invalid relative to . 




The  rule, where ' = , y_0, …, y_n, (,_0), …, (,_n):


' _0 : C, _0 : , …, _n : C, _n : ,

: ⩽ n  . C,


Assume, : ⩽ n  . C, is invalid relative to . From this, it follows that there exists an interpretation ℐ and a label assignment λ such that , ℐ, λ and ℐ, λ : ⩽ n  . C,. It follows that () ∈(⩾ (n+1) . C). Thus, there are at least n+1 many distinct elements a_0, …, a_n∈ such that (λ(x),a_i) ∈ and a_i∈C. We now define a new label assignment λ' such that λ'(z) = λ(z) if z ≠ y_i with 0 ≤ i ≤ n and λ'(y_i) = a_i. Hence, ℐ, λ' , y_0, …, y_n,  (,_0), …, (,_n) and ℐ, λ' _0 : C, …, _n : C, as λ'(y_i) ∈C for each 0 ≤ i ≤ n. Moreover, let y_i :  = y_i : D_1, … y_i : D_k for 0 ≤ i ≤ n. Since ⊤ D_j∈ for 1 ≤ j ≤ k, we have that , λy_0 : , …, y_n : as . Therefore, the premise is invalid relative to .


The  rule:



_i : C,  : ⩾ n  . C,  |  1 ≤ i ≤ n
, y_i y_j : ⩾ n  . C,  | 1 ≤ i < j ≤ n

: ⩾ n  . C,


Assume, : ⩾ n  . C, is invalid relative to . It follows that there exists an interpretation ℐ and a label assignment λ such that ℐ, λ and ℐ, λ : ⩾ n  . C,. We note that if n=0, then λ(x) ∉(⩾ 0  . C), which cannot be the case, and hence, we may suppose that n > 0. Then, we have that λ() ∈(⩽ (n-1) . C). From the side condition on , there are labels y_1, …, y_n such that xLy_i with L = (), which, by  <ref>, implies that (λ(x),λ(y_i)) ∈ for each 1 ≤ i ≤ n. If (y_i) ≠(y_j) for each 1 ≤ i < j ≤ n, then for some 1 ≤ i ≤ n, we have that λ(y_i) ∉C; otherwise, we have (y_i) = (y_j) for some 1 ≤ i < j ≤ n. The former cases show that at least one premise in the first set is invalid relative to  and the latter case shows that at least one premise in the second set of premises is invalid relative to .
 


<ref> The  rule is provable in , and the xy, , , , , and  rules are hp-admissible.


 Recall that ⊤ = A  A for some fixed A ∈. The proof below shows that  provable in .



𝕀
, x : A, x :  A

, x : A  A



The hp-admissibility of xy is shown by induction on the height of the given proof. The base cases are trivial as any application of xy to an initial rule yields another instance of the initial rule. In the inductive step, with the exception of the  and  cases, all cases are resolved by invoking IH and then applying the rule. In the  and  cases, the label substituted into the sequent may be fresh in the  or  inference, requiring two applications of IH in order for the case to go through. To demonstrate this, we show how a problematic  case is resolved and note that the  case is similar. Suppose we have an instance of  followed by yz as shown below left, where y is fresh in . The case is resolved as shown below right, where vy is applied in the first IH application with v fresh due to the side condition of the rule, yz is then applied in the second IH application, and last,  is applied.



, (,)  : C,  : ,

:  C,
yz
(y/z)  :  C, (y/z)


   

, (,)  : C,  : ,
IH
, (,v)  v : C, v : ,
IH
(y/z), (,v)  v : C, v : , (y/z)

(y/z)  :  C, (y/z)





The hp-admissibility of , , and  are shown by induction on the height of the given proof while making a case distinction on the last rule applied. The base cases are trivial as any application of either rule to 𝕀 or  yields another instance of the rule, and with the exception of the  case, every case of the inductive step may be resolved by applying IH followed by the corresponding rule. The  case is trivial when showing the hp-admissibility of  and , however, an interesting case arises when showing the hp-admissibility of . Suppose we have an application of  as shown below, which weakens in an equality y_i y_j that is active in the  application. Observe that the desired conclusion is obtained by taking the proof of the premise , y_i y_j : ⩾ n  . C,. All other cases where  is followed by an application of  are simple or resolved similarly.



_i : C,  : ⩾ n  . C,   |  1 ≤ i ≤ n
, y_i y_j : ⩾ n  . C,  |  1 ≤ i < j ≤ n

: ⩾ n  . C,

, y_i y_j : ⩾ n  . C,






The hp-admissibility of  is also shown by induction on the height of the given proof. We note that the hp-admissibility of  relies on the hp-admissibility of another contraction rule , shown below left, which `fuses' two children nodes in a sequent. The hp-admissibility of  and  is shown simultaneously by induction on the height of the given proof, though we focus on the  case as the  case is similar. Returning back to the proof that  is hp-admissible, we note that the base cases are trivial since any application of  to 𝕀 or  yields another instance of the rule. In the inductive step, if neither of the contraction formulae x : C, x : C are principal in the conclusion of a rule application (r), as shown in the example below right, then the case is resolved by applying IH (i.e. the  rule) and then the rule (r). 



, r(x,y), r(x,z)

(y/z), r(x,y) (y/z)


   

' ', x : C, x : C

(r)
, x : C, x : C

, x : C



Therefore, let us suppose that one of the contraction formulae x : C, x : C is principal. We consider the case where the last rule applied above  is the  rule, as shown below left. To resolve the case, we apply the hp-invertibility of , followed by the an application of  which applies (y/z), followed by a sufficient number of applications of IH for  to contract all of the displayed formulae in the consequent, and finally, an application of , as shown below right.



, r(x,y) , y : C, y : , x :  C


, x :  C, x :  C

, x :  C


   

, r(x,y) , y : C, y : , x :  C
Lem. <ref>
, r(x,y), r(x,z) , y : C, y : , z : C, z :

, r(x,y) , y : C, y : , y : C, y :
IH
, r(x,y) , y : C, y :

, x :  C



The remaining cases are solved in a similar fashion. Also, note that the proof of  <ref> does not rely on the hp-admissibility of  or , and therefore, the above argument is not circular.

Last, we argue the hp-admissibility of  by induction on the height of the given proof. The only interesting case is the  case in the base case; the base case for 𝕀 is trivial, and the inductive step follows in each case by applying IH followed by the rule. Suppose we have an instance of  as shown below left, where the side condition xy holds. Since xy holds yx by definition, we have that the application of  shown below right is a valid application of , thus showing  hp-admissible in this case.





, x  y, y  x

, y  x


   



, y  x



The other case when  is applied to a non-principal inequality in  is trivial.



<ref>
All non-initial rules in  are hp-invertible.


 The hp-invertibility of , , and  follows from the fact that  (and  in the  case) are hp-admissible (see Lemma <ref> above). The remaining cases are shown by induction on the height of the given proof. We only consider the  case since all other cases are analogous.


Base case. Suppose we have instances of 𝕀 and  as shown below.





: A,  :  A, ,  : ⩽ n  . C






, x  y ,  : ⩽ n  . C



The instance of 𝕀 shown below top and the instance of  shown below bottom resolve the base case. Note that we take ' = , w_0, …, w_n, (,w_0), …, (,w_n).




'  : A,  :  A, , w_0 : C, w_0 : , …, w_n : C, w_n :






', x  y , w_0 : C, w_0 : , …, w_n : C, w_n :



Inductive Step. We only consider the  and  cases as the remaining cases are similar.


. Suppose we have an instance of  as shown below left. We can resolve the case as shown below right, where ' = , w_0, …, w_n, (,w_0), …, (,w_n).



: L,  : L, ,  : ⩽ n  . C

: L, ,  : ⩽ n  . C


   

: L,  : L, ,   : ⩽ n  . C
IH
'  : L,  : L, , w_0 : C, w_0 : , …, w_n : C, w_n :

'  : L, , w_0 : C, w_0 : , …, w_n : C, w_n :






. There are two cases to consider when the last rule applied is . Either, the principal formula is the formula we want to invert, or it is not. In the first case, shown below, we simply take the proof of the premise, where ' = , y_0, …, y_n, (,_0), …, (,_n).


' _0 : C, _0 : , …, _n : C, _n : ,

: ⩽ n  . C,


In the second case, we simply apply IH and then the  rule to resolve the case.





<ref>[Completeness]
If ∅ : C, then ⊩∅ : ,  : C. 


 We describe a proof-search algorithm  that takes a sequent : ,  : C as input and attempts to construct a proof thereof. We assume that : ,  : C is not provable in  and show how to construct an interpretation = (,·) and define a label assignment  such that , ∅ : ,  : C, meaning  and (x) ∉C, that is, ∅ : C. Let us now begin our description of .


. We take  : ,  : C as input and move to the step below.


 and . Let _1, …, _n be all branches of the pseudo-proof  currently under construction. Let _1, …, _n be the top sequents of each branch, respectively. For each 1 ≤ i ≤ n, if _i is an instance of 𝕀 or , then apply  and , respectively, bottom-up on _i and close that branch, i.e. halt  on the branch _i. If  has halted on every branch, then return . Otherwise, if a sequent _i exists such that no rule from  is bottom-up applicable to it, copy it above itself and continue to step  below.




. Let _1, …, _n be all branches of the pseudo-proof  currently under construction. Let _1, …, _n be the top sequents of each branch, respectively. We consider each branch and its top sequent in turn. Let us suppose we have already considered _1, …, _i so that _i+1 is currently under consideration. Let the top sequent _i+1 be of the form:

    , _1 : L_1, …, _k : L_k

 with all labeled literals displayed. For each 1 ≤ i ≤ k and each y ∈() such that _iy, repeatedly apply the  rule bottom-up, extending _i+1. After all branches have been processed in this way, we move onto the  case below.



. Let _1, …, _n be all branches of the pseudo-proof  currently under construction. Let _1, …, _n be the top sequents of each branch, respectively. We consider each branch and its top sequent in turn. Let us suppose we have already considered _1, …, _i so that _i+1 is currently under consideration. Let the top sequent _i+1 be of the form:

    _1 : C_1 D_1, …, _k : C_k D_k,

 with all disjunctive formulae displayed. We repeatedly apply the  rule bottom-up, extending _i+1 so that it now has a top sequent of the form:
 
    _1 : C_1, _1 : D_1, …, _k : C_k, _k : D_k,

 After all branches have been processed in this way, we move onto the  case below.


. Let _1, …, _n be all branches of the pseudo-proof  currently under construction. Let _1, …, _n be the top sequents of each branch, respectively. We consider each branch and its top sequent in turn. Let us suppose we have already considered _1, …, _i so that _i+1 is currently under consideration. Let the top sequent _i+1 be of the form:

    _1 : C_1 D_1, …, _k : C_k D_k,

 with all conjunctive formulae displayed. We repeatedly apply the  rule bottom-up, extending _i+1 with 2^k new branches with each having a top sequent of the form:
 
    _1 : E_1, …, _k : E_k,

 where E_j∈{C_j,D_j} for 1 ≤ j ≤ k. After all branches have been processed in this way, we move onto the  case below.


. Let _1, …, _n be all branches of the pseudo-proof  currently under construction. Let _1, …, _n be the top sequents of each branch, respectively. We consider each branch and its top sequent in turn. Let us suppose we have already considered _1, …, _i so that _i+1 is currently under consideration. Let the top sequent _i+1 be of the form:

    _1 : ∃ r_1 . C_1, …, _k : ∃ r_k . C_k,

 with all existential formulae displayed. For each 1 ≤ j ≤ k and every label y ∈() such that _jLy with L = L_()(r_j), repeatedly apply the  rule bottom-up, extending _i+1. After all branches have been processed in this way, we move onto the  case below.

 
. Let _1, …, _n be all branches of the pseudo-proof  currently under construction. Let _1, …, _n be the top sequents of each branch, respectively. We consider each branch and its top sequent in turn. Let us suppose we have already considered _1, …, _i so that _i+1 is currently under consideration. Let the top sequent _i+1 be of the form:

    _1 : ∀ r_1 . C_1, …, _k : ∀ r_k . C_k,

 with all universal formulae displayed. For each 1 ≤ j ≤ k, repeatedly apply the  rule bottom-up, extending _i+1, and so the top sequent contains r_j(x_j,) in the antecedent and : C_j,  : in the consequent, where  is fresh for each j. After all branches have been processed in this way, we move onto the  case below.

 

. Let _1, …, _n be all branches of the pseudo-proof  currently under construction. Let _1, …, _n be the top sequents of each branch, respectively. We consider each branch and its top sequent in turn. Let us suppose we have already considered _1, …, _i so that _i+1 is currently under consideration. Let the top sequent _i+1 be of the form:

    _1 : (⩽ n_1_1 . C_1), …, _k : (⩽ n_k_k . C_k),

 with all qualified number restrictions of the form _j : (⩽ n_j_j . C_j) displayed and where 1 ≤ j ≤ k. We repeatedly apply the  rule bottom-up, extending _i+1 so that the top sequent contains y_0, …, y_n_j and (_j,y_0), …, (_j,y_n_j) in the antecedent and y_0 : C_j, _0 : , …, y_n_j : C_j, _n_j : in the consequent with y_0, …, y_n_j fresh for each considered qualified number restriction of the above form. After all branches have been processed in this way, we move onto the  case below.

 



. Let _1, …, _n be all branches of the pseudo-proof  currently under construction. Let _1, …, _n be the top sequents of each branch, respectively. We consider each branch and its top sequent in turn. Let us suppose we have already considered _1, …, _i so that _i+1 is currently under consideration. Let the top sequent _i+1 be of the form:

    _1 : (⩾ n_1_1 . C_1), …, _k : (⩾ n_k_k . C_k),

 with all qualified number restrictions of the form _j : (⩾ n_j_j . C_j) displayed and where 1 ≤ j ≤ k. For each collection {y_1, …, y_n_j}⊆(_i+1) of labels such that 
 _jLy_t with L = L_()(r_j) and 1 ≤ t ≤ n_j, we apply the  rule bottom-up, extending _i+1. After all branches have been processed in this way, we cycle back to the  and  case.

 
This concludes the description of .


 We know that  cannot return  since then a proof of : ,  : C would exist, contrary to our assumption. Therefore,  will not terminate, meaning that it constructs an infinite pseudo-proof  in the form of an infinite tree. Since only finite branches occurs within this pseudo-proof, by König's lemma we know that an infinite branch of the following form exists in :

    = (_0_0), (_1_1), …, (_n_n), …

 such that _0 = ∅ and _0 =  : ,  : C. Let us define ^* = ⋃_i ∈ℕ_i and ^* = ⋃_i ∈ℕ_i. We use  to construct an interpretation = (,·) and define a label assigment  such that , , ^*, but , ^*, meaning ∅ : C. We define = {[y]  |  y ∈() }, where we use [y] = [y]_^* for simplicity. In other words,  contains all equivalence classes modulo the =^*_^* relation on labels occurring in the sequents of the branch . We define  and · accordingly:



  * = [] for ∈();


  * [] ∈A :  A ∈^*;


  * ([],[]) ∈ either (1) there exist w ∈ [] and u ∈ [] such that (w,u) ∈^*, or (2) _1∘⋯∘_n∈ and ([]_i-1, []_i) ∈_i for 1 ≤ i ≤ n with ∈ [_0] and ∈ [_n]. 



Based on the definition above and the definition of an -system (), we note that if ([y],[z]) ∈, then there exist roles r_1, …, r_n and [z_1], …, [z_n-1] such that

    ^* [y] r_1 [z_1] r_2⋯ [z_n-1] r_n [z]

and r_1⋯ r_n∈ L_()(r). It is straightforward to show that  satisfies all RIAs _1∘⋯∘_n in . We now argue that , ^*. If r(y,z) ∈^*, then ([],[]) ∈ holds by the definition above, showing that ((),()) ∈. If y  z ∈^*, then by definition [y] = [z], showing (y) = (z). Also, observe that if y  z ∈^*, then it cannot be the case that [y] = [z] since then the  rule would be applied in , implying that  is finite, which is a contradiction as  is infinite; hence, (y) ≠(z). 

 We will now show that , ^*, and afterward, we will argue that  satisfies all GCIs in , thus establishing that . We argue by induction on the complexity of D that if y : D ∈^*, then (y) ∉D.




  y : A ∈^*. If y : A ∈^*, then for every z ∈ [y], z :  A ∉^* since otherwise  would have been applied, eventually followed by 𝕀 and  would be finite, contrary to our assumption. Therefore, y :  A ∉^*, implying that (y) ∉A by the definition of .



  y :  A ∈^*. Then, (y) ∈A, by the definition of .



  y : E  F ∈^*. Then, eventually the  rule will be applied in , meaning y : E, y : F ∈^*, showing that (y) ∈E and (y) ∈F by IH. Therefore, (y) ∈(E  F).



  y : E  F ∈^*. If y : E  F ∈, then eventually the  rule will be applied in , meaning either y : E ∈ or y : D ∈. Hence, either (y) ∈E or (y) ∈F by IH, implying (y) ∈(E  F).



  :  E ∈^*. Suppose ((y),(z)) ∈r, i.e. ([y],[z]) ∈r. It follows that [] L [z] with L = L_()(r), meaning at some step in , we have that []_L [z]_ with L = L_()(r). Hence, the  rule will be bottom-up applied, ensuring that : E ∈^*. By IH, we have that (z) ∉E, so since z was assumed arbitrary, we have that (y) ∉( E).



  :  E ∈^*. If :  E ∈^*, then eventually the  rule will be bottom-up applied in , ensuring that for some label z, r(y,z) ∈^* and : E ∈^*. By the definition of r, ([y],[z]) ∈r, and by IH (z) ∉E, thus (y) ∉ E.



  : ⩽ n r . E ∈^*. If : ⩽ n r . E ∈, then eventually the  rule will be applied bottom-up in . It follows that z_0, …, z_n, r(y,_0), …, r(y,_n) ∈^* and _0 : E, …, _n : E∈^*. Therefore, there exist at least n+1 distinct elements in , namely [y_0], …, [y_n], such that for 0 ≤ i ≤ n, ([y],[_i]) ∈r and where (z_i) ∉E_i by IH. Hence, (y) ∉(⩽ n r . E).



  y : ⩾ n r . E ∈^*. Assume that distinct [_1], …, [_n] ∈ exist such that for 1 ≤ i ≤ n, ([],[_i]) ∈. It follows that for 1 ≤ i ≤ n, [y] L [z_i] with L = () and z_1, …, z_n pairwise, distinct labels. Hence, at some step in , we have that yLz_i with L = (), and so, the  rule will be applied bottom-up, ensuring that z_i : E ∈^* for some 1 ≤ i ≤ n. By IH, (z_i) ∉E. Since the elements [_1], …, [_n] ∈ were assumed to be arbitrary and distinct, this shows that for any n elements that () relates to via , at least one must not be an element of E, i.e. () ∉(⩾ n r . E).


Let us now argue that  by arguing that all GCIs in  are satisfied on  (note that all RIAs are satisfied on  as stated above). Observe that our input is of the form : ,  : C and every time a fresh label is added by the  or  step of , the concepts in  are introduced at that label, meaning such concepts will occur at every label in (^*,^*). Therefore, by the argument above, we know that for every GCI ⊤ E ∈ and (y) = [y] ∈, (y) ∉E, showing that (y) ∈E, and hence, every GCI is satisfied on . As : C ∈^*, all of the above implies that ∅ : C, completing the proof.








§ PROOFS FOR  <REF>




<ref>
Let = _1∪_2 be an ontology 
and suppose that , Φ, Ψ_a, , , _b has a proof  in  with Φ∩Ψ = ∅. Then,  can be transformed into a proof in  of ; ΦΨ_a, , _b such that:



  (1) If x  y occurs in , then x  y ∈Φ ;


  (2) If x  y occurs in , then x  y ∈Ψ;


  (3) () ⊆(, Φ, Ψ, _a, , , _b); 


  (4) ⊆_a, ∩, _b.
 



 By induction on the height of the proof. The base cases are trivial, so we focus on the inductive step. We argue one of the  cases as the remaining cases are simple or similar. Suppose we have a proof in  ending with an application of , as shown below, where ' = , (,_0), …, (,_n) and let c ∈{a,b}.





', Φ,y_0, …, y_n, Ψ_a, , _0 : C, …, _n : C, , _b

, Φ, Ψ_a', ,  : ⩽ n  . C, , _b'





By IH, the premise of the inference shown below has a proof in , where _c = _c', _0 : _c, …, _n : _c for c ∈{a,b}. Since properties (1) and (2) hold for the premise below, and Φ∩ (y_0, …, y_n, Ψ) = ∅ by assumption, we know y_0, …, y_n∉(Φ, Ψ) since otherwise the side condition of the  application above would be violated. Hence,  will be in the form dictated by  <ref>, meaning we obtain a proof of the desired conclusion in  by a single application of , as shown below.




'; Φy_0, …, y_n, Ψ_a, _0 : C, …, _n : C, , _b

; ΦΨ_a',  : ⩽ n  . C, , _b' .




() ⊆(, Φ, Ψ, _a', , , _b') ∪{y_0, …, y_n} and ⊆_a, ∩y_0:C_0, …, y_n:C_n, , _b follow from IH with the latter also following from the fact that _c⊆_c. (1) and (2) easily hold, and as shown below, property (3) follows from the former fact:

    ( . )     =  () ∖{y_0, …, y_n}
       ⊆(, Φ, Ψ, _a', , , _b')
       ⊆(, Φ, Ψ, _a', ,  : ⩽n . C, , _b')


while property (4) follows from the latter fact:

    .  =   
       ⊆_a, ∩y_0 : C_0, …, y_n : C_n, , _b
        = _a, ∩ : ⩽ n  . C, , _b







<ref>
If () ∈, then there exists a () ∈ such that ⊆ and ⊆. 



 Let () ∈ and suppose for a contradiction that no () ∈ exists such that ⊆ and ⊆. Then, for each () ∈, either ⊈ or ⊈. Let = {(_1_1), …, (_n_n)} and define ' ' such that for each 1 ≤ i ≤ n, one and only one of the following holds: (1) x  y ∈' and x  y ∈_i∖, (2) x  y ∈' and x  y ∈_i∖, or (3) x : C∈' and x : C ∈_i∖. Observe that ∩' =∅ and ∩' =∅ by construction. However, since ' ' ∈ by  <ref>, we have that either ∩' ≠∅ or ∩' ≠∅, which gives a contradiction and proves the lemma.




<ref>
If ⊩; ΦΨ, then 



  * For each (' _i) ∈, ⊩, ', Φ, _i; 


  * For each (' _i) ∈, ⊩, ', Ψ_i,. 




 We prove both claims simultaneously by induction on the height of the proof and make a case distinction on the last rule applied.
 

Base case. Suppose we have a proof of height 1, i.e. an instance of an initial rule. Let us first consider the  case and then we will consider the  case, noting that the  case is similar.




; ΦΨ : A,  :  A, {(  : ⊤)}


Claim 1 is resolved as shown below left, and relies on  <ref>, whereas claim 2 is resolved by applying the  rule. Note that we use the interpolant = {( ⊢ : )} in claim 2 (see  <ref> above) and ' = ,  : A,  :  A.





, Φ,  : ⊤


   



, Ψ',  :





For the  case, suppose we have a proof consisting of a single application of the  rule, as shown below.




; ΦΨ, x  y  { (x  y  ) }


By the side condition on the rule, we know that xy holds for  above. Therefore, the application of  shown below left is warranted as is the application of  shown below right, thus resolving the case.





, Φ, x  y


   



, Ψ, x  y, x  y





Inductive step. For the inductive step, we consider the , , , and  cases as the remaining cases are similar.


. Let our proof in  end with an  application:


; ΦΨ

; ΨΦ


Observe that if (' _i) ∈, then , Ψ, ' , _i is provable in  by IH, which demonstrates claim (1). To prove claim (2), let (' _i) ∈. Then, by Lemma <ref>, there exists a (' _i') ∈ such that ' ⊆' and _i' ⊆_i. By IH, ⊩, Φ, ' _i',, implying ⊩, Φ, ' _i, by the hp-admissibility of , , and  (Lemma <ref>).


. Suppose we have a proof in  ending with an application of , as shown below.


; ΦΨ : C, _1
; ΦΨ : D, _2

; ΦΨ : C  D, _1∪_2


We prove claim (1) first. Let (' ) ∈_1∪_2. Regardless of if (' ) ∈_1 or (' ) ∈_2, we have a proof of , Φ, ' , by IH, which proves the claim. To prove claim (2), suppose that (_1, _2_1, _2) ∈_1∪_2 such that (_1_1) ∈_1 and (_2_2) ∈_2. By IH, the top two sequents below are provable in . We then apply the hp-admissibility of , , and  ( <ref>) a sufficient number of times (indicated by the asterisk) to ensure the contexts match. Last, we apply the  to obtain the desired conclusion.


, _1, Ψ : C, , _1
^*, ^*, ^*
, _1, _2, Ψ : C, , _1, _2

, _2, Ψ : D, , _2
^*, ^*, ^*
, _1, _2, Ψ : D, , _1, _2


, _1, _2Ψ : C  D, , _1, _2




. Suppose our proof ends with an  application:


, (,); ΦΨ : C,  : ,

; ΦΨ :  C,


 We first argue claim (1). Let (' , y : C_1, …, y : C_n) ∈ such that all concepts labeled with y are displayed and y ∉(') by assumption, and let = C_1, …, C_n. By IH, we obtain a proof in  ending as shown below: 


, ', r(x,y) , , y : C_1, …, y : C_n
× (n-1)
, ', (,) , , y :

, ' , ,  :


We now argue claim (2). Observe that for any (' ) ∈, the multiset  contains zero or more labeled concepts of the form x :  (C_1⋯C_n). We suppose  contains one such formula as the other cases are analogous, and let = ', x :  (C_1⋯C_n). The case is resolved as shown below, where ^* denotes n-1 applications of  between the n premises obtained from IH and ' =  : C,  : ,.



, ', (,) ', ', y : C_i |  1 ≤ i ≤ n
^*
, ', (,) ', ', y :

, ', (,)  : , ', ', y :

, ', (,)  : , ', '

, '  : ,  :  C, , '






. Let us suppose that we have a proof in  ending with an application of  as shown below such that ' = ,  (,_0), …, (,_n) and where ' = _0 : C, _0 : , …, _n : C, _n : ,.



'; ΦΨ, y_0, …, y_n'

; ΦΨ : (⩽ n  . C), .


We argue claim (1) first and suppose we have the following: (_1, _2, y_0 : _0, …, y_n : _n) ∈ such that _2⊆y_0, …, y_n, (_1) ∩{y_0, …, y_n} = ∅, and we let = _0, …, _n. By IH, the top sequent shown below has a proof in . We invoke  <ref> and apply the hp-admissible  and  rules  a sufficient number of times to derive the second sequent from the first, and then apply the  rule a sufficient number of times to obtain the third sequent from the second, using an asterisk * to indicate these sequential rule applications.




', Φ, _1, _2, , y_0 : _0, …, y_n : _n
^*, ^*
', Φ, _1, y_0, …, y_n, , y_0 : , …, y_n :
^*
', Φ, _1, y_0, …, y_n, , y_0 : , …, y_n :

, Φ, _1, , x :  .




Let us now argue claim (2). Observe if (”⊢) ∈., then  contains zero or more labeled concepts of the form x :  .. We suppose  contains one such formula and remark that the remaining cases are similar. Therefore, = ', x :  .. We let _i = C_i,1, …, C_i,k_i with 0 ≤ i ≤ n and = _0, …, _n. By IH, for each 0 ≤ i ≤ n, each top sequent shown below is provable in . We apply the  rule k_i-1 times, indicated by ^*,  to derive the second sequent from the first. 




', Ψ, y_0, …, y_n, ”', ', y_i : C_i,j |  1 ≤ j ≤ k_i
^*
', Ψ, y_0, …, y_n, ”', ', y_i : _i




We denote the concluding sequent in the proof above as _i'. Let us pick an 1 ≤ i ≤ n and let 1 ≤ℓ≠ i ≤ n. We then take _ℓ' and apply the hp-admissible rules zy_ℓ, y_ℓy_i, and y_iz with z fresh to obtain the sequent _ℓ”, shown below top, where the labels y_i and y_ℓ have been `swapped'. Observe that some inequalities of the form y_t y_s in y_0, …, y_n may have `flipped' to y_s y_t, yielding the set y_0, …, y_n. By applying  a sufficient number of times, one can weaken in all inequalities from y_0, …, y_n not occurring in y_0, …, y_n, and then apply  a sufficient number of times so that only y_0, …, y_n occurs in the antecedent. 




', Ψ, y_0, …, y_n, ”', ', y_i : _ℓ
^*
', Ψ, y_0, …, y_n, y_0, …, y_n, ”', ', y_i : _ℓ
^*
', Ψ, y_0, …, y_n, ”', ', y_i : _ℓ




For each 1 ≤ i ≤ n, we take _i' and each sequent proven as shown above, apply the  rule n-1 times, and then  to obtain a proof of the sequent _i as shown in the proof below. 




', Ψ, y_0, …, y_n, ”', ', y_i : _ℓ |  1 ≤ℓ≤ n
× n-1
', Ψ, y_0, …, y_n, ”', ', y_i :



', Ψ, y_0, …, y_n, ”', ',x : . , y_i :




Note that the last inference inference above is warranted since = by definition, and because  is hp-admissible by  <ref>. Next, observe that for each i and j such that 0 ≤ i < j ≤ n, the following sequent _i,j is provable by .






', Ψ, y_0, …, y_n, ”, y_i y_j', ', x : .





We can finish the proof of claim (2) as follows:




_0 ⋯ _n  _0,1 ⋯ _n,n+1
()

', Ψ, y_0, …, y_n, ”', ', x : .

, Ψ, ” : ⩽ n  . C, , ', x : .




This completes the proof of the lemma.







<ref>
If , is provable in  for all ( ⊢) ∈ and () = {}, then ⊩,  :. 


 Let := {(   x : C_i,1, …, x : C_i,k_i)  |  1 ≤ i ≤ n} and suppose that , x : C_i,1, …, x : C_i,k_i is provable in  for 1 ≤ i ≤ n. By repeated application of the  rule, we obtain , x: _1 ≤ j ≤ k_i C_i,j for each 1 ≤ i ≤ n. Applying the  rule n-1 times lets us prove , x: _1 ≤ i ≤ n_1 ≤ j ≤ k_i C_i,j, which gives us the desired conclusion. 




<ref>
If , is provable in  for all ( ) ∈ and () = {}, then ⊩,  :. 


 Let = {(  _1), …, (  _n)} such that _i = {x: C_i,1, …, x: C_i,k_i} for each 1 ≤ i ≤ n. We show ,  : is provable in  by induction on the cardinality of .
 

Base case. 
 Let us suppose that  is a singleton. Then, by assumption , x :  C_1,j is provable for all 1 ≤ j ≤ k_1, and so, the conclusion follows by k_1 - 1 applications of .


Inductive Step. Suppose that = {( _1), …, ( _n+1)} contains n+1 elements and assume that , is provable in  for all ∈. Then, for each 1 ≤ j ≤ k_n+1, the sequent , x : C_n+1,j, ' is provable in  for each (  ') ∈(∖{(  _n+1)}). By IH, for each 1 ≤ j ≤ k_n+1, the following sequent is provable in .

    , x : (∖{( _n+1)}), x: C_n+1,j

By applying the  rule between each of the k_n+1- 1 sequents above, followed by a single application of the (⊔) rule, we obtain a proof of

    , x : (∖{( _n+1)}) ⊔_1≤ j ≤ k_n+1C_n+1,j,

which gives our desired conclusion because

    = (∖{( _n+1)}) ⊔_1≤ j ≤ k_n+1C_n+1,j.





<ref>
Let = _1∪_2 be a  ontology. If C  D, i.e. , ⊩ C  D, then a concept interpolant I can be computed in  relative to  such that ⊩ C  I and ⊩ I  D, i.e. C  I and I  D.


 By our assumption and  <ref>, it follows that , ⊩ C  D, meaning x : , x : C D is the conclusion of  by definition. By  <ref>, namely, the hp-invertibility of the  rule, x : , x : C, x : D is provable in  with a proof '. By  <ref>, the interpolation sequent ∅; ∅∅ x : _1, x : C x : D, x : _2 is provable in  with () = {x} and ⊆_1, C∩D, _2. Moreover, as this interpolation sequent is free of (in)equalities, i.e. ,Φ, Ψ = ∅, we note that by the first two properties of  <ref>,  must be of the following form:

    = {(   x : C_i,1, …, x : C_i,k_i)  |  1 ≤ i ≤ n}.

 By Lemmas <ref> – <ref>, we have x : _1, x : C, x : I and x : _2, x : D, x : I are provable in  such that I =. Both of the sequents x : _1, x : C I and x : _2, x : I D are provable with proofs _1 and _2 in  by applying , respectively. By  <ref>, C  I and I  D.

Last, we argue that the computation of I is in  relative to the size of . Note that applying  <ref> is composed of the following steps: first, we partition the sequents in ' by starting with the conclusion of ' and working our way up the proof toward the initial sequents placing active formulae of rule instances within the same component of the partition as their corresponding principal formulae. Second, we assign interpolants to all of the initial sequents and work our way back down toward the conclusion of the proof by computing the interpolant of the conclusion of a rule from the interpolants of its premises, and applying the  when needed. The only problematic operation is the  rule as it may exponentially increase the size of interpolants, meaning the calculation of I may be exponential in the worst-case.





