The quotient operation from graph theory offers an elegant graph summarization framework that has been widely investigated in the literature, notably for the exploration and efficient management of large graphs; it consists in fusing equivalent vertices according to an equivalence relation.
In this paper, we study whether a similar operation may be used to summarize ABoxes. Towards this goal, we define and examine the quotient operation on an ABox: we establish that a quotient ABox is more specific than the ABox it summarizes, and characterize to which extent it is more specific. This preliminary investigation validates the interest of a quotient-based ABox summarization framework, and paves the way for further studies on it in the description logic setting, e.g., to devise equivalence relations suited to the optimization of typical data management and reasoning tasks on large ABoxes or to the visualization of large ABoxes, and on its utilization in related settings, e.g., Semantic Web.
Graph summarization has received considerable attention in the literature [14,5], in particular for the exploration and visualization of large graphs, as well as for the optimization of graph management systems (cardinality estimation, indexing, etc). A well-established tool used to summarize graphs into compact ones is the quotient operation from graph theory [12]; other kinds of summaries have also been considered like collections of graph statistics or of frequent graph patterns, or a mix of both as in [16].
The quotient operation offers an elegant graph summarization framework by decoupling the summarization method, which basically fuses equivalent vertices, from the high-level specification of equivalent vertices, defined by an equivalence relation, e.g., bisimilarity [1]. Applying the quotient operation to a graph results in a (typically small) homomorphic approximation of it, called quotient graph; the equivalence relation to choose depends on the target summary usage.
In this paper, we study whether a similar operation may be used to summarize ABoxes. Towards this goal, we first transfer the quotient operation from graphs to description logics (DLs) [2] in order to summarize ABoxes as if they were merely graphs. Then, because ABoxes are not just graphs but are essentially first-order theories (or slight extensions of them), we examine the semantics of the quotient operation on an ABox. We establish that a quotient ABox is more specific than the ABox it summarizes, by showing that its structure entails the structure of the ABox, and we characterize to which extent this quotient ABox is more specific than the ABox it summarizes, by determining the precise nature of the approximation between the quotient ABox contents and the ABox contents. This latter characterization is the main result of this paper. It provides an in-depth understanding of the quotient operation itself as a tool for ABox summarization; the essence of quotient ABoxes is independent of the DL under consideration and of the chosen equivalence relation (that depends on the target summary usage).
The paper is organized as follows. We recall the basics of DLs in Sec. 2. Then, we transfer the quotient operation from graphs to ABoxes in Sec. 3 and we examine its semantics w.r.t. DLs in Sec. 4. Finally, we discuss related works in Sec. 5 and we conclude with salient perspectives in Sec. 6.
The proofs of our technical results can be found in the appendix of this paper.
We recall the important aspects of DLs that are used in this paper [2], with a focus on the lightweight DL-lite R DL [4] that we (just) use to illustrate our discussions throughout this paper; our results hold for (standard) DLs.
DL syntax and semantics Given a set N C of concept names (unary predicates), a set N R of role names (binary predicates), and a set N I of individuals (constants), a DL allows expressing unary and binary formulae respectively called concepts and roles. They are used to build TBoxes (ontologies) made of concept inclusions of the form C 1 ⊑ C 2 and role inclusions of the form R 1 ⊑ R 2 , as well as to build ABoxes (databases) storing concept assertions of the form C(a) and role assertions of the form R(a 1 , a 2 ), where a, a 1 , a 2 ∈ N I . In DL-lite R , concepts and roles are built according to the following rules, where A ∈ N C and R ∈ N R :
Also, TBox inclusions are of the forms B ⊑ C and Q ⊑ S, while ABox assertions are of the forms A(a) and R(a 1 , a 2 ).
First-order interpretations are used to define the semantics of DLs. They are of the form I = (∆ I , • I ), where ∆ I is a non-empty domain and • I is a function that maps every a ∈ N I to a I ∈ ∆ I , every A ∈ N C to A I ⊆ ∆ I , and every R ∈ N R to R I ⊆ ∆ I × ∆ I . Further, the interpretation function • I is extended to the concept and role formulae allowed in the DL under consideration. In DLlite R , • I is extended as follows:
) holds, and it satisfies a TBox iff it satisfies all the TBox inclusions. I satisfies an assertion C(a
The main data management tasks are consistency checking and query answering. They involve an ABox A and may rely on the knowledge of a TBox T . A is consistent w.r.t. T iff A has a model that is also a model of T . To query ABoxes, we consider the first-order language of unions of conjunctive queries that is widely-considered for ontology-mediated query answering [3] and ontology-based data access [17]. A conjunctive query (CQ) is of the form ∃ ⃗ Y ϕ, where ϕ is a conjunction of the forms A(t) or R(t, t ′ ) where t, t ′ are variables or constants, and ⃗ Y is a tuple of variable from ϕ. A CQ is Boolean if all its variables are existentially quantified. The answer to a Boolean CQ q is true if it is entailed by A and T , denoted A |= T q, i.e., q is true in all the models of A and T ; otherwise q is false. The answer to a non-Boolean CQ q with free variables X 1 , . . . , X n , i.e., of arity n, is the set of all the tuples of constants of the form ⃗ a = ⟨a 1 , . . . , a n ⟩ such that A |= T q[⃗ a], where q[⃗ a] is the Boolean CQ obtained by replacing each X k by a k for 1 ≤ k ≤ n. We note q A,T the answer set of q on A w.r.t. T , with the convention that for Boolean queries q A,T = ∅ if q is f alse, and q A,T = {⟨⟩} if q is true where ⟨⟩ is the empty tuple. A union of CQs (UCQ) is a disjunction of CQs with same arity. The answer to a UCQ is the union of the answers to its individual CQs.
An ABox A can be represented, and is frequently drawn, as a multigraph with typed vertices and typed edges: the vertices are the constants in A, there is a vertex type C on the vertex a iff the concept assertion C(a) is in A, and there is an R-typed edge a R → a ′ iff the role assertion R(a, a ′ ) is in A. Based on this analogy, we transfer the quotient operation from graphs to ABoxes to define quotient ABoxes.
Definition 1 (Quotient ABox). Let A be an ABox, ≡ be some equivalence relation between constants, and let a 1 ≡ , . . . , a n ≡ denote by a slight abuse of notation both the equivalence classes of the constants in A w.r.t. ≡ and the names of these equivalence classes. The quotient ABox of A w.r.t. ≡ is the ABox A ≡ such that:
In this paper, we do not focus on particular equivalence relations between constants (i.e., binary relations that are reflexive, symmetric and transitive), though in the description logic setting we consider they should be defined w.r.t. an ABox and a TBox. Discussing DL-specific equivalence relations between constants is delegated to future work.
ULab(l 1 ), CLab(l 2 )} which states that s is a PhD student (PhDS), who is jointly supervized by (sB) the researchers (R) r 1 , who works for (wF) the university lab (ULab) l 1 , and r 2 , who works for the company lab (CLab) l 2 and who also works with (wW) r 1 .
The graph representations of A ex and of three of quotient ABoxes obtained from it are depicted in Fig. 1. The equivalence relations used in this figure somehow reflect that equivalent constants are instances of the same concept for Fig. 1(b), or instances of non-disjoint concepts with a common generalizing concept if we assume that company labs and university labs are not necessarily disjoint kinds of labs for Fig. 1(c), i.e., CLab ⊑ Lab ∈ T ex and ULab ⊑ Lab ∈ T ex , and if we further assume that PhD student and researcher are not necessarily disjoint kinds of employees for Fig. 1(d), i.e., PhDS ⊑ Emp ∈ T ex and R ⊑ Emp ∈ T ex .
In the sequel, we term summary of an ABox A a quotient ABox of A.
Although Definition 1 does enable the quotient-based summarization of an ABox, an ABox is not just a graph because it also has a first-order semantics. An important question that therefore arises is: does there exist a semantic relationship between an ABox and a summary of it? To answer this question we first point out that, in Definition 1, the implicit function that maps the constants in A to the constants in A ≡ defines a homomorphism from A to A ≡ ; from now, we name this function h and we say that an ABox constant a is represented by a summary
constant a ≡ iff h(a) = a ≡ holds. Based on this ABox-to-summary homomorphism, we answer the above question by relating an ABox and a summary of it through entailment between ABoxes w.r.t. a TBox. The property below states that if we compare an ABox and a summary of it through entailment regardless of the constants they use (they are incomparable otherwise because they use different sets of constants), by just considering how the ABox (resp. summary) atoms join according to these constants, then the ABox is more general than its summary.
Property 1. Let T be a TBox, a 1 , . . . , a m be the constants in an ABox A and a 1 ≡ , . . . , a n ≡ be the constants in some summary A ≡ of A. If we consider these constants as existential variables, then
Besides, it is also worth noting that, due to the existence of the ABox-tosummary homomorphism, an ABox and a summary of it are related through the essential data management tasks of consistency checking and query answering. Property 2. Let T be a TBox, A be an ABox and A ≡ be some summary of A.
Property 3. Let T be a TBox, A be an ABox, A ≡ be some summary of A, and let q be a UCQ. If q A,T ̸ = ∅ holds then q A≡,T h ̸ = ∅ holds, with q h the query q in which every constant a is replaced by its image h(a) through the A-to-A ≡ homomorphism h.
We remark that Property 2 and the contraposition of Property 3 (i.e., if q A≡,T h = ∅ holds then q A,T = ∅ holds) are of practical interest to check rapidly if, for sure, an ABox is consistent and if a query has no answer, by using the typically (much) smaller ABox summary.
Example 2 (Cont.). From now, let us assume that T ex just consists of the inclusions mentioned in Example 1.
To illustrate Property 1, it is easy to see on Fig. 1 that A i ≡ |= ∅ A ex holds for i ∈ {b, c, d}, hence holds with |= Tex .
As for Property 2, it is also easy to see that A i ≡ is consistent w.r.t. T ex , for i ∈ {b, c, d}, as well as A ex . We remark that if PhD students and researchers would be disjoint, i.e., PhDS ⊑ ¬R ∈ T ex , then A d ≡ would be inconsistent w.r.t. T ex while A ex would be consistent w.r.t. T ex . This observation indicates that DL-specific equivalence relations should avoid to the extent possible building inconsistent summaries out of consistent ABoxes.
Finally, let us illustrate Property 3 on Fig. 1. Consider the UCQ q = R(X) ∧ wF(X, l 1 )∪R(X)∧wF(X, l 2 ) asking for the researchers who work for the lab l 1 or l 2 .
q has some answer on A ex w.r.t. T ex (q Aex,Tex = {⟨r 1 ⟩, ⟨r 2 ⟩}), thus its translation q h has some answer w.r.t. T ex on the summary A i ≡ , i ∈ {b, c, d}. For the CQ q = PhDS(X 1 ) ∧ wW(X 1 , X 2 ) asking for the PhD students and people with whom they work, we note that because the q h translation does not have answers on A i ≡ w.r.t. T ex , i ∈ {b, c}, i.e., q
= ∅, hence by contraposition of Property 3, q does not have answer on A ex w.r.t. T ex either, i.e., q Aex,Tex = ∅. However, we observe that q h has some answer on A d ≡ w.r.t. T ex , while q has no answer on A ex w.r.t. T ex , i.e., this particular summary fails in detecting that q has no answer on A ex w.r.t. T ex . This observation suggests that DL-specific equivalence relations should be carefully chosen depending on the target summary usage.
Resuming our initial discussion, though Property 1 states that a summary is more specific than the ABox it summarizes up to the set of constants they use, it immediately raises a second crucial question: to which extent a summary is more specific than the original ABox it summarizes? We answer this second question by characterizing to which extent the knowledge a summary has about a constant is more specific than the knowledge the ABox has about the equivalence class this summary constant represents, and similarly for a pair of summary constants and the pair of equivalence classes these summary constants represent in the ABox.
For an ABox A and a TBox T , the most precise knowledge about a set of constants a 1 , . . . , a n corresponds to one or more concepts known as the most specific concepts (MSCs) a 1 , . . . , a n are all instances of [2]. A concept C is a MSC of a 1 , . . . , a n w.r.t. A and T iff (i) A |= T C(a i ) holds for all i ∈ [1, n], and (ii) for any concept D such that A |= T D(a i ) holds for all i ∈ [1, n], either C ⪯ T D holds or C ̸ ⪯ T D and D ̸ ⪯ T C hold. We remark that though a MSC may be of infinite size in some DLs, this is not an issue here as we just want a semantic characterization of it. In the sequel, we designate by msc A,T (a 1 , . . . , a n ) the conjunction (⊓) of the MSCs of a 1 , . . . , a n w.r.t. A and T 1 and we refer to it as the MSC of a 1 , . . . , a n w.r.t. A and T , because it always exists (the empty conjunction is the universal concept ⊤) and it is obviously unique up to equivalence.
A first step towards answering our second question is Lemma 1, which provides an upper approximation through subsumption of the MSC of some summary constant w.r.t. the individual MSCs of the equivalent ABox constants it represents; Lemma 1 follows from the existence of the ABox-to-summary homomorphism.
Lemma 1. Let T be a TBox, A be an ABox and A ≡ be the summary of A w.r.t. the ≡ equivalence relation. If a 1 , . . . , a n are all the constants in A that belong to the equivalence class a ≡ according to ≡, then the following holds:
≡ of A ex in Fig. 1 and illustrate Lemma 1 with the summary constant l 1 |l 2 and the ABox constants l 1 , l 2 it represents:
At the same time, in the above Lemma 1, to the set of (equivalent) constants a 1 , . . . , a n corresponds its most specific concept msc A,T (a 1 , . . . , a n ), as recalled above. As the next step towards answering our second question, Lemma 2 provides a lower approximation through subsumption of the MSC of a 1 , . . . , a n w.r.t. the individual MSCs of these constants; it follows from the definition of MSC.
Lemma 2. Let T be a TBox and A be an ABox. If a 1 , . . . , a n are constants in A, then the following holds:
≡ of A ex in Fig. 1 and illustrate Lemma 2 with the summary constant l 1 |l 2 and the ABox constants l 1 , l 2 it represents like in the preceding example: msc Aex,Tex (l 1 , l 2 ) = Lab ⊓ ∃wF − , and ⊔ x∈{l1,l2} msc Aex,Tex (x) ⪯ T msc Aex,Tex (l 1 , l 2 ), i.e., (ULab ⊓ ∃wF − ) ⊔ (CLab ⊓ ∃wF − ) ⪯ Tex Lab ⊓ ∃wF − , clearly holds.
We are now ready to answer our second question with Theorem 1, which is a direct corollary of Lemma 1 and Lemma 2. It relates msc A,T (a ≡ ) and msc A,T (a 1 , . . . , a n ) through their respective upper and lower approximations.
Theorem 1. Let T be a TBox, A be an ABox and A ≡ be the summary of A w.r.t. the ≡ equivalence relation. If a 1 , . . . , a n are all the constants in A that belong to the equivalence class a ≡ according to ≡, then the following holds:
From Theorem 1, it is now clear that the semantic distance through subsumption between the knowledge about each constant a ≡ in the summary, i.e., msc(a ≡ ), and the knowledge about the set of equivalent constants that a ≡ represents in the ABox, i.e., msc A,T (a 1 , . . . , a n ), corresponds at least to approximate the union of individual knowledge about a 1 , . . . , a n in the ABox by a conjunction, i.e., approximating n i=1 msc A,T (a i ) by n i=1 msc A,T (a i ). We establish similar results (omitted due to space limitations) by adapting the notion of MSC to roles.
Finally, we stress that all the above results just follow from the definition of quotient ABox (Definition 1). In particular, they are independent of the equivalence relation (≡) and of the DL under consideration.
We present below the works from the DL literature that are closely related to ABox summarization.
An ABox summarization approach for the SHIN DL has been studied to optimize consistency checking [8] and instance retrieval in the subsequent work [6], i.e., finding the instances of a given SHIN concept; these two summary-based optimizations are implemented in the SHER system [7]. This approach can be seen as a particular instantiation for the SHIN DL of our general ABox summarization framework, in which equivalent constants are non-distinct constants2 stored in the ABox as instances of the same SHIN concepts; our framework allows using this definition of equivalent constants for the equivalence relation ≡ or any other relevant to the target summary usage. We therefore provide a better understanding of the SHIN summaries of [8,6,7] by establishing that they are more specific than the SHIN ABoxes they summarize, and notably to which extent they are more specific. Further, we remark that our ABox summarization approach, because it is based on the quotient operation, is more declarative than that of [8,6,7], by elegantly decoupling the summarization means (i.e., fusing equivalent constants) from the high-level specification of equivalent constants, i.e., the equivalence relation ≡ to use. By contrast, SHIN summaries are defined by an explicit canonical function that maps ABox constants to summary one; our function h has similar goal but is implicit because derived from the ABox and equivalence relation at hand.
Another form of ABox summarization is ABox abstraction, which has been studied for materialization in the Horn-ALCHOI and Horn-SHOIF DLs [9,10],
i.e., for pre-computing and storing entailed assertions. The idea is to represent several assertions of an ABox by a single one in the ABox abstraction. To this aim, an ABox B is defined as an abstraction of an ABox A if there exists a mapping from the constants in B to the constants in A that defines a homomorphism from B to A. Hence, by contrast with our summaries that are more specific than original ABoxes, abstractions are more general than original ABoxes, thus capture a subset of their contents.
Also related to ABox summarization is ABox modularization, which has been studied for instance retrieval in the SHIF [13] and SHI [15] DLs. It consists in extracting a subset of an ABox that entails all the assertions in which a given constant is involved.
Finally, less related works on ABox summarization do not summarize an ABox by another, e.g., [16] which computes statistics about the concept and roles instances, and Abstract Knowledge Patterns of the form (C 1 , r, C 2 ) indicating that the role r relates instances of the concept C 1 to instances of the concept C 2 .
We devised a well-founded ABox summarization framework for DLs, by applying the quotient operation from graph theory to ABoxes and examining the quotient ABoxes, i.e., summaries, it produces.
With this now well-understood ABox summarization framework in place, the next necessary step is to study DL-specific equivalence relations between constants, to explore, visualize or optimize reasoning on and the management of ABoxes. These equivalence relations might be sought either from scratch or derived from the ones used for graph summarization if meaningful w.r.t. the DL semantics, e.g., the well-established and widely adopted ones based on bisimilation [14] or the recent ones based on the cooccurrence of types and edges [11]. Also, ideally, such relations should be devised to avoid to the extent possible building inconsistent summaries out of consistent ABoxes (recall Example 2).
≡ ) ∈ A ≡ and 1 ≤ i ≤ n, and such that (ψ(a i ≡ ), ψ(a j ≡ )) ∈ R I for every R(a i ≡ , a j ≡ ) ∈ A ≡ and 1 ≤ i, j ≤ n. Let us consider the composite function ψ • h, where ψ is the above function and h is the implicit function that defines our ABox-to-summary homomorphism. This function thus maps a 1 , . . . , a m to the interpretation domain of I and clearly ψ(h(a i )) ∈ C I for every C(a i ) ∈ A and 1 ≤ i ≤ m, because by construction of A ≡ C(h(a i )) ∈ A ≡ , and such that (ψ(h(a i )), ψ(h(a j ))) ∈ R I for every R(a i , a j ) ∈ A and 1 ≤ i, j ≤ m, because by construction of A ≡ R(h(a i ), h(a j )) ∈ A ≡ . Therefore, I is also a model of ∃a Consider the model J = (∆ J , • J ) defined as follows: ∆ J = ∆ I , A J = A I for every concept name A ∈ N C , R J = R I for every role name R ∈ N R , and for every constant a in A, a J = h(a) I .
For every concept assertion C(a) ∈ A, C(h(a)) ∈ A ≡ by definition of a quotient ABox, where h is the implicit function defining the ABox-to-summary homomorphism. Since I is a model of A ≡ , I is a model of C(h(a)), i.e., h(a) I ∈ C I . By definition of J , C J = C I and a J = h(a) I , thus a J ∈ C J , i.e., J is a model of C(a). J is therefore a model of all the concept assertions in A.
Similarly, for every role assertion R(a k , a l ) ∈ A, R(h(a k ), h(a l )) ∈ A ≡ by definition of a quotient ABox, where h is the implicit function defining the ABox-to-summary homomorphism. Since I is a model of A ≡ , I is a model of R(h(a k ), h(a l )), i.e., (h(a k ) I , h(a l ) I ) ∈ R I . By definition of J , R J = R I , a J k = h(a k ) I and a J l = h(a l ) I , thus (a J k , a J l ) ∈ R J , i.e., J is a model of R(a k , a l ). J is therefore a model of all the role assertions in A.
It therefore follows that J is a model of all the assertions in A, hence a model of A. ⊓ ⊔ Proof (Proof of Property 3). We remark that if a query is asked on an ABox that is inconsistent w.r.t. its associated TBox, then both true and f alse if the query is Boolean, and all the tuples of the arity of the query otherwise, are answers. If A is not consistent w.r.t. T , then q A,T ̸ = ∅, and by the contraposition of Property 2, A ≡ is not consistent w.r.t. T too, therefore q A≡,T h ̸ = ∅ and Property 3 holds in this first case.
If A is consistent w.r.t. T , while A ≡ is not consistent w.r.t. T (see Example 2), then Property 3 holds in this second case: q A≡,T h ̸ = ∅ holds whenever q A,T ̸ = ∅ or q A,T = ∅ holds.
Otherwise, A is consistent w.r.t. T and A ≡ is consistent w.r.t. T . Let us show that Property 3 holds in this third and last case. If the UCQ q has a non-empty answer set, then at least one of its CQs has a non-empty answer set. Let q ′ be such a CQ in q. Let us assume, without loss of generality, that q ′ is Boolean as the definition of non-Boolean query answers reduces to the Boolean case. Let us consider some model J of A ≡ and T . Let I be the interpretation such that ∆ I = ∆ J , A I = A J for every concept name A ∈ N C , R I = R J for every role name R ∈ N R , and a I = h(a) J for every constant a in A. Clearly, by construction, I is homomorphic to J and is a model of A and T . Thus, I is also a model of q ′ . Further, J is obviously a model of q ′ just in case q ′ does not contain contants, because the constants in A do not have interpretations in J : ∆ I = ∆ J , A I = A J for every concept name A ∈ N C , R I = R J for every role name R ∈ N R . Otherwise, J is a model of q ′ h , in which constants from A are replaced by the constants in A ≡ they are represented by: a I = h(a) J for every constant a in A. Therefore, every model of A ≡ and T is a model of q ′ h , i.e., q ′ h is entailed by A ≡ and T , thus has a non-empty answer set, hence q h has a non-empty answer set too. ⊓ ⊔ Proof (Proof of Lemma 1 Otherwise, both A and A ≡ are consistent w.r.t. T , and let us consider some model J of A ≡ and T . Let I be the interpretation such that ∆ I = ∆ J , A I = A J for every concept name A ∈ N C , R I = R J for every role name R ∈ N R , and a I = h(a) J for every constant a in A. Clearly, by construction, I is homomorphic to J and is a model of A and T . Because I is a model of A and T , I is a model of the concept assertion (msc A,T (a i ))(a i ) for 1 ≤ i ≤ n. By construction of I, J is a model of (msc A,T (a i ))(h(a i )) for 1 ≤ i ≤ n, where h is the ABox-to-summary homomorphism, i.e., J is a model of (msc A,T (a i ))(a ≡ ) for 1 ≤ i ≤ n.
It follows that all the models of A ≡ and T are models of (msc A,T (a i ))(a ≡ ) for 1 ≤ i ≤ n, and of (msc A≡,T (a ≡ ))(a ≡ ) ( * ). By definition of the MSC of a ≡ , either (i) msc A≡,T (a ≡ ) ⪯ T n i=1 msc A,T (a i ) holds or (ii) msc A≡,T (a ≡ ) ̸ ⪯ T n i=1 msc A,T (a i ) and n i=1 msc A,T (a i ) ̸ ⪯ T msc A≡,T (a ≡ ) hold. In the latter case (ii), msc A≡,T (a ≡ )⊓ n i=1 msc A,T (a i ) would be strictly subsumed by msc A≡,T (a ≡ ) w.r.t. T , and because of ( * ) above, msc A≡,T (a ≡ ) ⊓ n i=1 msc A,T (a i ) would be the MSC of a ≡ , a contradiction. Therefore, we must be in case (i) and msc A≡,T (a ≡ ) ⪯ T In particular, it is well-known that msc A,T (a 1 , . . . , a n ) and lcs T (msc A,T (a 1 ), . . . , msc A,T (a n )) are equivalent [2]. Further, it is also known that lcs T (msc A,T (a 1 ), . . . , msc A,T (a n )) cannot be more specific than n i=1 msc A,T (a i ), notably they are equivalent in DLs allowing disjunction (⊔). Thus, n i=1 msc A,T (a i ) ⪯ T msc A,T (a 1 , . . . , a n ) holds. ⊓ ⊔
This work was partially supported by the ANR project CQFD (ANR-18-CE23-0003).
Proof (Proof of Property 1). In case ∃a