Query answering in lattice-based description logic
Krishna Manoorkar Ruoding Wang

[
    [
    
=====



§ ABSTRACT 
Recently, the description logic LE-𝒜ℒ𝒞 was introduced for reasoning in the semantic environment of the enriched formal contexts, and a tableaux algorithm was developed for checking the consistency of ABoxes in this logic <cit.>. In this paper, we study the ontology-mediated query answering in LE-𝒜ℒ𝒞. In particular, we show that several different types of queries can be answered efficiently for LE-𝒜ℒ𝒞  knowledge bases with acyclic TBoxes using our tableaux algorithm directly or by extending it with some additional rules. 




§ INTRODUCTION

Description logic (DL) <cit.> is a class of logical formalisms, rooted in classical first-order logic, widely used in Knowledge Representation and Reasoning to articulate and infer relationships among pertinent concepts within a specified application domain. It is widely utilized across various fields such as the semantic web <cit.>, ontologies <cit.>, and software engineering <cit.>. Description logic offers solutions to diverse reasoning tasks arising from a knowledge base. Among the notable reasoning services offered by description logic is ontology-mediated query answering, which involves answering queries based on a given knowledge base <cit.>. 

In <cit.>[We noticed a  mistake in the proof of termination and I-compatibility in an earlier version of this paper <cit.> in which concepts ⊤ and  were included as concept names. In the updated version <cit.> we prove that the result holds in the restriction which does not contain ⊤ and  in the language of concept names. In this paper, we work with the restricted language as in <cit.>.], a two-sorted lattice-based description logic LE-𝒜ℒ𝒞[Even though concept names in  LE-𝒜ℒ𝒞 do not contain negation, we still refer to this description logic as LE-𝒜ℒ𝒞 rather than LE-𝒜ℒℰ, as negation on ABox terms is included in the description logic language.] was introduced based on non-distributive modal logic, with semantics grounded in an enriched formal context <cit.>. LE-𝒜ℒ𝒞 provides a natural description logic to reason about formal concepts (or categories) arising from formal contexts in Formal Concept Analysis (FCA) <cit.>. The logic LE-𝒜ℒ𝒞 has the same relationship with non-distributive modal logic and its semantics based on formal contexts as the relationship between 𝒜ℒ𝒞 and the classical normal modal logic with its Kripke frame semantics. Namely, LE-𝒜ℒ𝒞  facilitates the description of enriched formal contexts, i.e., formal contexts endowed with additional relations, which give rise to concept lattices extended with normal modal operators. Similarly to the classical modal operators, the `non-distributive' modal operators can be given different interpretations, such as the epistemic operator <cit.> and the approximation operator <cit.>. 

In this paper, we adapt and modify the LE-𝒜ℒ𝒞 tableaux algorithm provided in <cit.> to answer several different types of queries based on LE-𝒜ℒ𝒞  knowledge bases with acyclic TBoxes. We show that for any consistent LE-𝒜ℒ𝒞 ABox 𝒜, the model constructed from the tableaux completion of 𝒜 is a universal or canonical model for answering different queries like relationship queries asking if an object and a feature are related, membership  queries asking if an object or a feature belongs to a concept, and subsumption queries asking if a concept is included in some other concept. This allows to answer multiple such queries in polynomial time in |𝒜|. We show that it also acts as a universal model w.r.t. negative relational queries, however this is not true for negative membership or subsumption queries.

Finally, we consider separation queries which ask if two objects or features can be distinguished from each other by means of some role (relation). We convert these queries into an equivalent problem of checking the consistency of the given ABox w.r.t. some extension of LE-𝒜ℒ𝒞 and providing a tableaux algorithm for such extension. This method allows to answer separation queries of  different types in polynomial time in |𝒜|. 
 

Structure of the paper. In Section <ref>, we briefly review non-distributive modal logic and polarity-based semantics, lattice-based description logic LE-𝒜ℒ𝒞, and tableaux algorithm for checking its ABox consistency. In Section <ref>, we demonstrate that the model obtained from the Tableaux Algorithm (Section <ref>) is a universal model for various queries, and define different types of queries and corresponding algorithms. Section <ref> provides a specific LE-𝒜ℒ𝒞 knowledge base and illustrates how the algorithms answer queries discussed earlier. Finally, Section <ref> summarizes the paper and outlines future directions.



§ PRELIMINARIES

In this section, we collect preliminaries on non-distributive modal logic and its polarity-based semantics, i.e. semantics based on formal contexts, and the lattice-based description logic LE-𝒜ℒ𝒞 with the tableaux algorithm developed for it in <cit.>. 



 §.§ Basic non-distributive modal logic and its polarity-based semantics

In this section, we briefly introduce the basic non-distributive modal logic and polarity-based semantics for it. It is a member of a family of lattice-based logics, sometimes referred to as LE-logics (cf. <cit.>), which have been studied in the context of a research program on the logical foundations of categorization theory <cit.>. 
Let  be a (countable) set of atomic propositions. The language ℒ is defined as follows:

φ|⊤| p |φ∧φ|φ∨φ|φ|φ,  


where p∈. In the following part, we define the polarity-based semantics for this logic.





The basic, or minimal normal ℒ-logic is a set 𝐋 of sequents ϕ⊢ψ, with ϕ,ψ∈ℒ, containing the following axioms:




     p ⊢ p             ⊢ p             p ⊢ p ∨ q             p ∧ q ⊢ p             ⊤⊢⊤             p ∧ q ⊢(p ∧ q)
     

                 p ⊢⊤             q ⊢ p ∨ q             p ∧ q ⊢ q             ⊢             (p ∨ q) ⊢ p ∨ q





and closed under the following inference rules:

		
		
    ϕ⊢χ  χ⊢ψ/ϕ⊢ψ  ϕ⊢ψ/ϕ(χ/p)⊢ψ(χ/p)  χ⊢ϕ  χ⊢ψ/χ⊢ϕ∧ψ  ϕ⊢χ  ψ⊢χ/ϕ∨ψ⊢χ  ϕ⊢ψ/ϕ⊢ψ  ϕ⊢ψ/ϕ⊢ψ




Relational semantics.
 
The following preliminaries are taken from <cit.>.
For any binary relation T⊆ U× V, and any U'⊆ U  and V'⊆ V,  we let[For any u ∈ U (resp. v ∈ V) we will sometimes write T^(1)[u] (resp. T^(0)[v]) in place of T^(1)[{u}] (resp. T^(0)[{v}]).]



T^(1)[U']{v|∀ u(u∈ U'⇒ uTv) }     T^(0)[V']{u|∀ v(v∈ V'⇒ uTv)}.




A polarity or formal context (cf. <cit.>) is a tuple ℙ =(A,X,I), where A and X are sets, and I ⊆ A × X is a binary relation. 

A and X can be understood as the collections of objects and features, and for any a∈ A and x∈ X, aIx exactly when the object a has the feature x. For any formal context ℙ = (A, X, I), the pair of maps 
 
 (·)^↑: 𝒫(A)→𝒫(X) and (·)^↓: 𝒫(X)→𝒫(A),



defined by B^↑ I^(1)[B] and Y^↓ I^(0)[Y],
[For any a ∈ A (resp. x∈ X) we will sometimes write a^↑ and a^↑↓ (resp. x^↓ and x^↓↑) in place of {a}^↑ and {a}^↑↓ (resp. {x}^↓ and {x}^↓↑).],
forms a Galois connection, and hence induces the closure operators(·)^↑↓ and (·)^↓↑ on 𝒫(A) and on 𝒫(X), respectively. 

A formal concept of a polarity ℙ=(A,X,I) is a tuple c=(c,c) such that c⊆ A and c⊆ X, and c = c^↓ and c = c^↑,  
i.e. the sets c and c are  Galois-stable. The set of formal concepts of polarity ℙ, with the order defined by

c_1 ≤ c_2   iff  c_1⊆c_2  iff  c_2⊆c_1,


forms a complete lattice ℙ^+, namely  the concept lattice of ℙ. 


An enriched formal ℒ-context is a tuple 𝔽 =(ℙ, R_, R_), where R_⊆ A × X and R_⊆ X × A are I-compatible relations, that is, for all a ∈ A and x ∈ X, the sets R_^(0)[x], R_^(1)[a], R_^(0)[a], R_^(1)[x] are Galois-stable in ℙ. 
Given the operations [R_] and ⟨ R_⟩ on ℙ^+ corresponding to R_ and R_, respectively, we have for any c ∈ℙ^+,


[R_] c =(R_^(0)[c], I^(1)[R_^(0)[c]])   and  ⟨ R_⟩  c =( I^(0)[R_^(0)[c]], R_^(0)[c]).


We refer to the algebra 𝔽^+=(ℙ^+, [R_], ⟨ R_⟩) as the complex algebra of  𝔽. A valuation on such an 𝔽
is a map V→ℙ^+. For each p∈, we let pV(p) (resp. pV(p)) denote the extension (resp. intension) of the interpretation of p under V.

A model is a tuple 𝕄 = (𝔽, V), where 𝔽 = (ℙ, R_, R_) is an enriched formal context and V is a valuation of 𝔽. For every ϕ∈ℒ, we let ϕ_𝕄V(ϕ) (resp. ϕ_𝕄V(ϕ)) denote the extension (resp. intension) of the interpretation of ϕ under the homomorphic extension of V.   The `satisfaction'  and `co-satisfaction' relations ⊩ and ≻  can be recursively defined as follows: 





𝕄, a ⊩ p     iff a∈p_𝕄    
𝕄, x ≻ p     iff x∈p_𝕄 

𝕄, a ⊩⊤     always    
𝕄, x ≻⊤     iff   a I x for all a∈ A

𝕄, x ≻     always    
𝕄, a ⊩     iff a I x for all x∈ X

𝕄, a ⊩ϕ∧ψ     iff 𝕄, a ⊩ϕ and 𝕄, a ⊩ψ     
𝕄, x ≻ϕ∧ψ     iff (∀ a∈ A) (𝕄, a ⊩ϕ∧ψ⇒ a I x)


𝕄, x ≻ϕ∨ψ     iff  𝕄, x ≻ϕ and 𝕄, x ≻ψ     𝕄, a ⊩ϕ∨ψ     iff (∀ x∈ X) (𝕄, x ≻ϕ∨ψ⇒ a I x).




As to the interpretation of modal operators: 





𝕄, a ⊩ϕ      iff (∀ x∈ X)(𝕄, x ≻ϕ⇒ a R_ x)       
𝕄, x ≻ϕ      iff (∀ a∈ A)(𝕄, a ⊩ϕ⇒ a I x)


𝕄, x ≻ϕ      iff (∀ a∈ A) (𝕄, a ⊩ϕ⇒ x R_ a)       
𝕄, a ⊩ϕ     iff (∀ x∈ X)(𝕄, x ≻ϕ⇒ a I x).  






The definition above ensures that, for any ℒ-formula φ,


𝕄, a ⊩ϕ   iff   a∈ϕ_𝕄,     and     𝕄,x ≻ϕ   iff   x∈ϕ_𝕄. 





𝕄ϕ⊢ψ   iff   ϕ_𝕄⊆ψ_𝕄  iff    ψ_𝕄⊆ϕ_𝕄. 


The interpretation of the propositional connectives ∨ and ∧ in the framework described above reproduces the standard notion of join and meet of formal concepts used in FCA. The interpretation of operators  and  is motivated by algebraic properties and duality theory for modal operators on lattices (see <cit.> for an expanded discussion). 
In <cit.>, it is shown that the semantics of LE-logics is compatible with Kripke semantics for classical modal logic, and thus, LE-logics are indeed generalizations of classical modal logic.
This interpretation is further justified in <cit.> by noticing  that, under 
the interpretations of the relation I as 
a I x iff “object a  has feature x”
and  R=R_ =R^-1_ as a R x iff “there is evidence that object a  has feature x”, then, for any concept c, the extents of concepts c and c can be interpreted as “the set of objects which certainly belong to c” (upper approximation), and “the set of objects which possibly belong to c” (lower approximation) respectively. Thus, the interpretations of  and  have similar meaning in the LE-logic as in the classical modal logic.


 §.§ Description logic LE-𝒜ℒ𝒞


In this section, we recall the lattice-based description logic LE-𝒜ℒ𝒞 introduced in <cit.> as a counterpart of non-distributive modal logic. 

The language of LE-𝒜ℒ𝒞 contains two types of individuals, usually interpreted as objects and features. Let 𝖮𝖡𝖩 and 𝖥𝖤𝖠𝖳 be disjoint sets of individual names for objects and features. The set ℛ of the role names for LE-𝒜ℒ𝒞 is the union of three types of relations: (1) a unique relation I ⊆𝖮𝖡𝖩×𝖥𝖤𝖠𝖳; (2) a set of relations ℛ_  of the form R_⊆𝖮𝖡𝖩×𝖥𝖤𝖠𝖳; (3) a set of relations ℛ_ of the form R_⊆𝖥𝖤𝖠𝖳×𝖮𝖡𝖩. The relation I is intended to be interpreted as the incidence relation of formal contexts and encodes information on which objects have which features, and the relations in ℛ_  and ℛ_ encode additional relationships between objects and  features (see <cit.> for an extended discussion). In this paper, we work with an LE-𝒜ℒ𝒞 language in which the sets of role names ℛ_ and ℛ_ are singletons. All the results in this paper can be generalized to language with multiple role names in each of these sets straightforwardly.

For any set  𝒟 of atomic concept names, the language of LE-𝒜ℒ𝒞 concepts is:

C  D | C_1 ∧ C_2 | C_1∨ C_2 | ⟨ R_⟩ C | [R_ ]C   


where D ∈𝒟.


This language matches the LE-logic language and has an analogous intended interpretation of the complex algebras of the enriched formal contexts (cf. Section <ref>).
As usual, ∨ and ∧ are to be interpreted as the smallest common superconcept and the greatest common subconcept, as in FCA. 
 



 We do not use the symbols ∀ r and ∃ r in the context of LE-𝒜ℒ𝒞 because using the same notation verbatim would  be ambiguous or misleading, as the semantic clauses of modal operators in LE-logic use universal quantifiers. 

TBox assertions in LE-𝒜ℒ𝒞 are of the shape C_1 ≡ C_2[As is standard in DL (see <cit.> for more details), general concept inclusions of the form C_1 ⊑ C_2 can be rewritten as C_1 ≡ C_2 ∧ C_3, where C_3 is a new concept name.], where C_1 and C_2 are concepts defined as above. 
ABox assertions are of the form:


aR_ x,   xR_ a,   aIx,   a:C,   x::C,  α,  


where α is any of the first five ABox terms. We refer to the first three types of terms as relational terms. We denote an arbitrary ABox (resp. TBox) with 𝒜 (resp. 𝒯). The interpretations of the terms a:C and x::C are: “object a is a member of concept C”, and  “feature  x is in the description of concept C”, respectively. Note that we explicitly add negative terms to ABoxes, as the concept names in LE-𝒜ℒ𝒞 do not contain negations. 


An interpretation for LE-𝒜ℒ𝒞 is a tuple ℳ = (𝔽, ·^ℳ), where 𝔽=(ℙ, R_, R_) is
an enriched formal context, and ·^ℳ maps:

1. individual names a ∈𝖮𝖡𝖩 (resp. x ∈𝖥𝖤𝖠𝖳)   to some a^ℳ∈ A (resp. x^ℳ∈ X);

2. role names I, R_ and R_ to  relations I^ℳ⊆ A× X, R_^ℳ⊆ A× X and R_^ℳ⊆ X× A in 𝔽;

3. any atomic concept D to D^ℳ∈𝔽^+, and other concepts as follows:



     
    (C_1 ∧ C_2)^ℳ = C_1^ℳ∧ C_2^ℳ       (C_1∨ C_2)^ℳ = C_1^ℳ∨ C_2^ℳ    
    ([R_]C)^ℳ = [R_^ℳ]C^ℳ       (⟨ R_⟩ C)^ℳ =⟨  R_^ℳ⟩ C^ℳ

    


where the all the connectives are interpreted as  defined as in LE-logic  (cf. Section <ref>). The satisfiability relation for an interpretation ℳ is defined as follows:

1. ℳ C_1≡ C_2 iff C_1^ℳ = C_2^ℳ iff C_2^ℳ = C_1^ℳ.

2. ℳ a:C iff a^ℳ∈C^ℳ
and  ℳ x::C iff x^ℳ∈C^ℳ.

3. ℳ  a I x (resp. a R_ x, x R_ a) iff a^ℳ I^ℳ x^ℳ (resp. a^ℳ R_^ℳ x^ℳ, x^ℳ R_^ℳ a^ℳ). 

4. ℳα,  where α is any ABox term, iff ℳα. 


The satisfaction definition  can be extended to concept inclusion as follows. For any concepts C_1, and C_2, and an interpretation ℳ,  ℳ C_1 ⊑ C_2 iff C_1^ℳ≤ C_2^ℳ. 


An interpretation ℳ is a model  for an  LE-𝒜ℒ𝒞 knowledge base (𝒜, 𝒯)
if  ℳ𝒜 and ℳ𝒯.
 




 §.§ Tableaux algorithm for checking LE-𝒜ℒ𝒞 ABox consistency


In this section, we  introduce the   tableaux algorithm for checking the consistency of LE-𝒜ℒ𝒞 ABoxes. An LE-𝒜ℒ𝒞 ABox 𝒜 contains a clash iff it contains both β and β for some relational term β. The expansion rules below are designed so that 
the expansion of 𝒜 will contain a clash iff  𝒜 is inconsistent. 
The set   sub(C) of sub-formulas of 
  any  LE-𝒜ℒ𝒞   concept name C  is defined  as usual. A concept name C' ∈𝒜 (in symbol: C' ∈𝒜) if C'∈ sub(C) for some C such that  one of the terms a:C,  x::C, (a:C), or (x ::C) is in 𝒜. A constant b  (resp. y) occurs in 𝒜 (b ∈𝒜, or y ∈𝒜), iff some term containing b (resp. y) occurs in it. 


The tableaux algorithm below constructs a model 
(𝔽,·^ℳ) for every consistent 𝒜, where 𝔽= (ℙ, R_, R_) is such that, for any C ∈𝒜, some a_C ∈ A and x_C ∈ X exist such that, for any a ∈ A (resp. any x ∈ X), a ∈C^ℳ (resp. x ∈C^ℳ) iff a I x_C (resp. a_C I x).
We call a_C and x_C the classifying object and the classifying feature of C, respectively.[To make the notation easily readable, we write a_ C, x_ C (resp. a_ C, x_ C) instead of a_[R_]C, x_[R_]C (resp. a_⟨ R_⟩ C, x_⟨ R_⟩ C).] The commas in each rule are meta-linguistic conjunctions, hence every tableau is non-branching. 


 





 
1cCreation rule     1cBasic rule 

For any C ∈𝒜
create
a_C:C,   x_C::C
      
[-1.85mm]0mm8mm
b:C,    y::C
I
b I y











2cRules for the logical connectives     2cI-compatibility rules 

[-1.85mm]0mm8mm
 b:C_1 ∧  C_2
∧_A
b:C_1,   b:C_2
     
y::C_1 ∨  C_2
∨_X
y::C_1,   y::C_2
       
b I  y
y
b R_ y


     
b I ▪ y
▪ y
y R_ b



 b:[R_]C,   y::C

b R_ y
      
  y::⟨  R_⟩ C,   b:C

y R_ b
     b I  y
b
y R_ b
     b I y
b
b R_ y





2cinverse rule for connectives  


   b:C_1, b:C_2, C_1 ∧ C_2 ∈𝒜
∧_A^-1
b:C_1 ∧ C_2
     y::C_1, y::C_2, C_1 ∨ C_2 ∈𝒜
∨_X^-1
y::C_1 ∨ C_2


2cAdjunction rules  

[-1.85mm]0mm8mm
b R_ y
R_
b I y,   b I  y
      
y R_ b
R_
b I y,   b I ▪ y

 [2mm]



2cBasic rules for negative assertions     2cAppending  rules 

[-1.85mm]0mm8mm
(b:C)
b
(b I x_C)
      
(x::C)
x
(a_C I x)
      
b I x_C
x_C
b:C
      
a_C I y
a_C
y::C







In the adjunction rules, the individuals b, b, y,   and ▪ y are new and unique individual names[The new individual names b, b, y,   and ▪ y appearing in tableaux expansion are purely syntactic entities.  Intuitively, they correspond to the classifying objects (resp. features) of the concepts b, b (resp. y, resp. ▪y),  where 𝐛=(b^↑↓, b^↑) (resp. 𝐲=(y^↓, y^↓↑)) is the concept generated by b (resp. y),  and  the operation   (resp.▪) is the left (resp. right) adjoint of operation  (resp. ).]  for each relation R_ and R_, and individuals b and y, except for  a_C= a_ C and x_C= x_ C. 











It is easy to check that the following rules are derivable in the calculus. 


b:C_1 ∨ C_2,   y::C_1,   y::C_2
∨_A
b I y
       

 y::C_1 ∧  C_2,   b:C_1,   b:C_2
∧_X
b I y


b:C
adj_
b: [R_] C
      
▪ y::C
adj_
y::⟨ R_⟩  C








The following theorem follows from the results in <cit.>:

The tableaux algorithm <ref> provides a sound and complete polynomial-time decision procedure for checking consistency of  LE-𝒜ℒ𝒞 ABoxes. 


For any consistent LE-𝒜ℒ𝒞 ABox 𝒜, 
we construct a model ℳ =(𝔽,·^ℳ) from the tableaux completion 𝒜  of 𝒜, where 𝔽 =(A,X,I,R_,R_) is described as follows:
A and X are taken to be the sets of all individual names of object and feature that occur in 𝒜, respectively, and all individuals are interpreted by their names. For any role name R, its interpretation R^ℳ is defined as follows: for any individual names l, m, l R^ℳ m iff l R m ∈𝒜. Finally, for the atomic concept D, its interpretation is set to the concept (x_D^↓, a_D^↑). The following result was proved in <cit.>.


For any LE-𝒜ℒ𝒞 ABox 𝒜, the model ℳ as constructed above is a model for 𝒜 of the size polynomial in |𝒜|. Moreover, for any individual names b, y, and concept C occurring in 𝒜, b ∈C iff b I x_C ∈𝒜, and y ∈C iff a_c I y ∈𝒜. 



    The algorithm can be easily extended to acyclic TBoxes (exponential-time), using the unraveling technique (see <cit.> for details).

In this paper, we use LE-𝒜ℒ𝒞 knowledge bases to mean LE-𝒜ℒ𝒞 knowledge bases with acyclic Tboxes unless otherwise stated. 



 §.§ Ontology-mediated query answering

A key task in description logic ontologies (knowledge bases) is to support various reasoning tasks, one of which is to answer queries based on ontologies <cit.>.
Let 𝒦 =(𝒜, 𝒯) be a consistent knowledge base given in a specific description logic DL. Given a query q(p) (with a possibly empty tuple of free variables p) in (appropriate) first-order language and a model ℳ of 𝒦, we say that a sequence of individuals a in 𝒜 is an answer for query q(p) w.r.t. model ℳ of knowledge base 𝒦 if ℳ q(a). An answer a in 𝒜 is said to be a certain answer for the query q(p)  w.r.t. a knowledge base 𝒦 if it is an answer for q(p) w.r.t. all the models of 𝒦. An important notion used in ontology-mediated query answering is that of a universal or canonical model. For a query q(p) on a knowledge base 𝒦, we say that a model ℳ of 𝒦 is a universal or canonical model for 𝒦  if for any a appearing in 𝒦, 𝒦 q(a) iff ℳ q(a).[In case p is empty, the answer or the certain answer for such query is true or false depending on whether ℳ q or not.] Thus, we can provide certain answer for query q over  𝒦 by only looking over the universal or canonical model ℳ. Universal models for different description logics have been extensively studied <cit.>.  In this paper, we would focus on answering some specific types of queries over knowledge bases in non-distributive description logic LE-𝒜ℒ𝒞. To this end, we show that for any LE-𝒜ℒ𝒞 ABox 𝒜, the model constructed from it by applying the LE-𝒜ℒ𝒞 tableaux algorithm <ref> acts as the universal model for 𝒜 w.r.t. several different types of queries. As the tableaux algorithm is polynomial in time and produces a polynomial size model in |𝒜|, this provides a polynomial-time algorithm to answer these types of queries.








§ QUERY ANSWERING OVER LE-𝒜ℒ𝒞 ABOXES

In this section, we discuss  different types of queries pertaining to  LE-𝒜ℒ𝒞 ABoxes and develop algorithms to answer them.  We start by showing that for any consistent LE-𝒜ℒ𝒞 ABox 𝒜, the model obtained  using Algorithm <ref> behaves like universal model w.r.t. several types of queries. 



 §.§ Universal model for LE-𝒜ℒ𝒞 ABox

For any  individual name appearing in the tableaux expansion 𝒜 of an LE-𝒜ℒ𝒞 ABox 𝒜 , we define its concept companion as follows :

1. For any constant b (resp. y) appearing in 𝒜,  con(b) (resp. con(y)) is a concept such that for any interpretation ℳ,  con(b)^ℳ = 𝐛 (resp. con(y)^ℳ = 𝐲), where 𝐛 (resp. 𝐲) denotes the concept generated by b^ℳ (resp. y^ℳ), i.e. 𝐛=((b^ℳ)^↑↓, (b^ℳ)^↑) (resp. 𝐲=((y^ℳ)^↓, (y^ℳ)^↓↑)). 

2. For any constant b (resp. b, resp. ▪ y, resp. y) appearing in 𝒜,  con( b)=  con(b) (resp. con( b)=  con(b), resp. con(▪ y)= ▪ con(y), resp. con( y)=  con(y)), where the operation  (resp. ▪) is the left (resp. right) adjoint of  (resp. ). 
 
 
For any consistent LE-𝒜ℒ𝒞 ABox 𝒜,  individual names b, y appearing in its completion 𝒜, and concept  C appearing in 𝒜:




   1. 𝒜  con(b) ⊑   con(y)  iff b I y ∈𝒜,      2. 𝒜  con(b) ⊑ con (y)  iff b R_  y ∈𝒜, 

   3. 𝒜 con(b) ⊑   con (y)  iff y R_  b ∈𝒜,      4. 𝒜  con(b) ⊑   C  iff b I x_C ∈𝒜, 

   5. 𝒜  C ⊑  con(y)  iff a_C I y ∈𝒜,     6. 𝒜  con(b) ⊑  C  iff b:C ∈𝒜, 

   7. 𝒜  C ⊑  con(y)  iff y::C ∈𝒜,     8. 𝒜  C_1 ⊑  C_2  iff a_C_1 I x_C_2∈𝒜. 

 




The proofs from left to right for items 1-5 follow immediately from  Theorem <ref>. We prove the right to left implications by simultaneous (over all the items) induction on the number of expansion rules applied. The base case is when the term in the right appears in 𝒜. In this case, it is immediate from the definition that we get the required condition on the left. 

    Creation rule. By this rule, a_C : C and x_C :: C are added by any C∈𝒜, which imply C⊑ C.

    Basic rule. By this rule, bIy is added from b:C and y::C. By induction applied to items 6 and 7, we get con(b)⊑ C and C⊑ con(y), which imply that con(b)⊑ con(y). It is easy to check item 4 and item 5 also hold. For item 8, a_C_1 I x_C_2 is added from a_C_1:C and x_C_2::C. By induction applied to items 6 and 7, we have C_1⊑ C and C⊑ C_2, which imply that C_1⊑ C_2.

    Rules ∧_A,  ∨_X, ∧_A^-1, ∨_X^-1. We give the proofs for rules ∧_A and ∧_A^-1. The proofs for ∨_X and ∨_X^-1 are analogous. 
    By rule ∧_A, b:C_1 and b:C_2 are added from b:C_1∧ C_2. By induction applied to item 6, con(b)⊑ C_1∧ C_2, and thus con(b)⊑ C_1 and con(b)⊑ C_2. 
    
 
    By rule ∧^-1_A, b:C_1∧ C_2 is added from b:C_1, b:C_2, and C_1∧ C_2∈𝒜. By induction applied to item 6, we have con(b)⊑ C_1 and con(b)⊑ C_2. Since C_1∧ C_2 exists in 𝒜, we get con(b)⊑ C_1∧ C_2.
    
    
    I-compatibility rules. We give the proofs for rules y and ▪ y. The proofs for b and b are analogous. 
    By rule y, b R_ y is added from b I  y, by induction applied to item 1, we get con(b)⊑ con( y) and by definition we have con(b)⊑ con(y). 
    
    By rule ▪ y, y R_ b is added from b I ▪ y. By induction applied to item 1, we have con(b)⊑ con(▪ y), and by definition con(b)⊑▪ con(y). By adjunction, we have con(b)⊑ con(y).
    
    
    Rules  and . We give the proof for rule , and the proof for  is analogous. By rule , b R_ y is added from b:[R_]C and y::C. By induction applied to item 6, we have con(b)⊑ C. By induction on item 7, we get C⊑ con(y). As  is a monotone operator, we have C⊑ con(y). Thus, con(b)⊑ con(y). 
    

    Adjunction rules. We give the proof for rule R_ and the proof for R_ is analogous. By rule R_, b I  y (resp. b I y) is added from b R_ y. By induction applied to item 2, we have con(b)⊑ con(y) (resp. con(b)⊑ con(y) by adjunction), and thus con(b)⊑ con( y) (resp. con( b)⊑ con(y)).
    

    Appending rules. By rule x_C, the term b:C is added from b I x_C. By induction applied to item 4, we have con(b)⊑ C. By rule a_C, y::C is added from a_C I y and by induction applied to item 5, we have C⊑ con(y).



Lemma <ref> implies that for any consistent ABox 𝒜, the model generated from 𝒜 using Algorithm <ref> acts as a universal model for several types of queries. We describe some such queries below.

Relationship queries. These queries are either Boolean queries asking if two individuals are related by  relation I, R_ or R_, e.g. q= b I y, or queries asking for names of all individuals appearing in 𝒜 that are related to some element by  relation I, R_ or R_, e.g. q(p)= b R_ p. 

Membership queries. These queries are either Boolean queries asking if some object or feature belongs to a given concept, e.g. q= y::C, or queries asking for names of all individuals appearing in 𝒜 that are in the extension or intension of a concept C, e.g. q(p)=p:C. 

Subsumption queries. These queries are Boolean queries asking if a concept C_1 is included in C_2, i.e. q=C_1 ⊑ C_2.[Note  no  non-trivial subsumptions are implied by knowledge bases with acyclic TBoxes. However, we include such queries as the algorithm can be used to answer queries regarding trivial (those implied by logic) subsumption efficiently. Moreover, we believe that the algorithm  extend ideas used to answer these queries may be used in future generalizations to knowledge bases with cyclic TBoxes.]

As Algorithm <ref> is polynomial-time and gives a model which is of polynomial-size in  |𝒜|, we have the following corollary. 


 For any LE-𝒜ℒ𝒞  ABox 𝒜, a query q of the above forms consisting of concepts and individual names appearing in 𝒜, can be answered in polynomial time in |𝒜| using Algorithm <ref>. 


    Relationship, membership, and subsumption queries can also be answered in polynomial time by converting them into a problem of consistency checking (see <cit.> for more details). However, it involves performing tableaux expansion for each query, while our result implies that we can answer multiple Boolean and naming queries with a single run of tableaux algorithm. 

If a subsumption or membership query has  concept C not appearing in 𝒜, we can answer such query by adding C to 𝒜 through creation rule i.e. adding terms a_C:C, and x_C::C to 𝒜. If we have multiple queries consisting of concepts not appearing in 𝒜, we can add all of these concepts  simultaneously and answer all queries with a single run of the tableaux algorithm.  




Disjunctive relationship and membership queries. A disjunctive relationship (resp. membership) query is formed by taking the 
disjunction of a finite number of relationship (resp. membership) queries, e.g. q=b I y ∨ b I z, and q(p)= p:C_1 ∨ p:C_2[The symbol ∨ in this paragraph  refers to join in the first-order (meta) language, and not join of concepts in LE-𝒜ℒ𝒞.].  The following lemma implies that we can answer such queries in LE-𝒜ℒ𝒞 by answering each disjunct separately.


Let t_1 and t_2 be any LE-𝒜ℒ𝒞 ABox terms not containing negation. Then, for any consistent LE-𝒜ℒ𝒞 ABox  𝒜,  𝒜 t_1 ∨ t_2  iff 𝒜 t_1 or 𝒜 t_2.


    𝒜 t_1 ∨ t_2 iff 𝒜∪{ t_1,    t_2} is inconsistent. By tableaux algorithm for  LE-𝒜ℒ𝒞, we have 𝒜∪{ t_1,    t_2}= 𝒜∪  B, where the only terms in B are t_1, t_2, and the terms obtained by applying the negative rule b or x to these terms. Therefore, as 𝒜∪{ t_1,    t_2} is inconsistent, 𝒜∪  B must contain a clash. But as 𝒜 is consistent, 𝒜 does not contain any clash. Therefore, some term in 𝒜 clashes with t_1 or t_2 or the term obtained by applying negative rule b or x to these terms. This implies that 𝒜∪{ t_1} or 𝒜∪{ t_1} must be inconsistent. Therefore, we have 𝒜 t_1 or 𝒜 t_2. 





 §.§ Negative queries

Negative queries are obtained by applying negation to relationship, membership and subsumption queries discussed above. These queries ask if the given ABox implies that some object is not related to some feature or some object (resp. feature) does not belong to some concept, or that one concept is not included in another concept. We start with negative relationship queries.


For any consistent LE-𝒜ℒ𝒞 ABox 𝒜 and for any individual names b and y,

1. 𝒜 (b I y) iff  (b I y)∈𝒜, 

2. 𝒜 (b R_ y) iff  (b R_ y) ∈𝒜,

3. 𝒜 (y R_ b) iff (y R_ b) ∈𝒜. 




We only prove items 1 and 2. The proof for item 3 is similar. For item 1, the right to left implication is trivial. For the left to right implication, suppose 𝒜 (b I y). Then, 𝒜∪{b I y}  must be inconsistent. As b and y appear in 𝒜, no tableaux expansion rule has the term b I y in its premise. Therefore, the tableaux completion of 𝒜∪{b I y} is 𝒜∪{b I y}. As 𝒜 is consistent, 𝒜 does not contain clash. Therefore, since 𝒜∪{b I y} must contain a clash, we have (b I y) ∈𝒜. However, note that no tableaux expansion rule can add such term for individual names b, y appearing in the original ABox 𝒜. Therefore, (b I y) ∈𝒜.

For item 2, the right to left implication is also trivial. For the left to right implication, suppose 𝒜 (b R_ y). Then, 𝒜∪{b R_ y}  must be inconsistent. As b and y appear in 𝒜, the only tableaux expansion rule having term b R_ y in its premise is adjunction rule R_ which adds terms b I y and b I  y. Again, the only rules that have any of these terms in premise are I-compatibility rules that add b R_ y to the tableaux expansion. Therefore, the tableaux completion of 𝒜∪{b R_ y} is 𝒜∪{b R_ y,   b I y, b I  y}. As 𝒜 is consistent, 𝒜 does not contain a clash. Therefore, as 𝒜∪{b R_ y,  b I y, b I  y} must contain a clash, one of the terms (b R_ y), (  b I y) or ( b I  y) must be in 𝒜. However, no expansion rule can add the terms of any of these forms. Furthermore, the terms of the form ( b I y) or (b I  y) cannot appear in the original ABox 𝒜. Therefore, (b R_ y) must be in 𝒜. 



As a result, we can answer negative relationship queries over a consistent  LE-𝒜ℒ𝒞 ABox 𝒜 in linear time by searching through 𝒜. 

We cannot apply a similar strategy to membership queries of the form (b:C) or (y::C), as such terms can be implied by 𝒜 without being present in 𝒜. For example, consider ABox 𝒜 = {b:C_1,  (b:C_1 ∧ C_2)} which implies (b:C_2), but this term does not appear in 
𝒜. This means that the model obtained by tableaux algorithm is not a universal model for these types of queries. Hence, to answer queries of the form (b:C) or (y::C), we must proceed by the usual route of adding the terms b:C or y::C to 𝒜 and checking the consistency of the resulting ABox.
We can also consider negative subsumption queries, i.e. queries asking whether the given ABox 𝒜 implies one concept C_1 is not included in another concept C_2, denoted as (C_1⊑ C_2).
Answering this query is the same as answering if the knowledge base obtained by adding the TBox axiom C_1⊑ C_2 to ABox 𝒜  is consistent. We can answer these queries for any TBox term C_1⊑ C_2, such that no sub-formula of C_1 appears in C_2, by using unraveling on C_1⊑ C_2, and then applying Algorithm <ref>. 

In this and previous sections, we have discussed answering Boolean queries of all the forms which an LE-𝒜ℒ𝒞 ABox term can take. Hence, we can combine these methodologies to answer ontology equivalence queries asking if two ABoxes are equivalent, i.e. 𝒜_1 ≡𝒜_2, by checking if every term in 𝒜_2 is implied by 𝒜_1 and vice versa. 




 §.§ Separation and differentiation queries

An important set of queries is queries  asking if the given knowledge base implies (ensures) that two individuals can be differentiated from each other by a certain property. In this section, we consider some queries of this type in LE-𝒜ℒ𝒞. 


Separation queries are queries of the form S(b,d)=∃ p (b I p ∧ (d I p)) or S(y,z)= ∃ p (p I y ∧ (p I z))  for two object (resp. feature) names b, d (resp. y, z) appearing in a given ABox. These queries can be understood as asking whether two given objects or features can be separated for sure using relation I based on the given knowledge base. Note that for any 
LE-𝒜ℒ𝒞 ABox 𝒜,

1.  𝒜∃ p(b I p ∧ (d I p))  iff 𝒜∪{∀ p(b I p ⇒ d I p)} is consistent, and 

2. 𝒜∃ p (p I y ∧ (p I z))  iff 𝒜∪{∀ p (p I y ⇒ p I z)} is consistent. 


Therefore, a separation query S(b,d) (resp. S(y,z)) can be answered by checking if 𝒜 is consistent in the extension of LE-𝒜ℒ𝒞 with the axiom ∀ p (b I p ⇒ d I p) (resp. ∀ p (p I y ⇒ p I z)). To this end, we consider the expansion of the LE-𝒜ℒ𝒞 tableaux algorithm with the rules 


b I x
SA(b,d)
d I x
     a I y
SX(y,z)
a I z
.






The tableaux algorithm obtained by adding the rule SA(b,d) (resp. SX(y,z)) to the LE-𝒜ℒ𝒞 tableaux expansion rules provides a polynomial-time sound and complete decision procedure for checking the consistency of 𝒜∪∀ p (b I p ⇒ d I p)(resp. 𝒜∪∀ p(p I y ⇒ p I z)). 


See Appendix <ref>. 


Hence, we can use this expanded tableaux algorithm to answer separation queries over a given ABox 𝒜 in polynomial time. This also allows us to answer differentiation queries Dif(b,d) = S(b,d) ∧ S(d,b) (resp. Dif(y,z) = S(y,z) ∧ S(z,y)) which ask if 𝒜 implies that b and d (resp. y and z) can be differentiated from each other by the relation I in polynomial time. We can similarly define and answer the separation and differentiation queries for the relations R_ and R_. Furthermore, we can answer identity queries asking if 𝒜 implies that two individuals are not identical by checking if they can be differentiated by some relation.

The strategy used to answer separation queries can also be used to answer many other interesting types of queries. For example, we can consider separation queries which ask about separation between different relations. Consider the queries SA(R_, R_, b) = ∃ p (b R_  p ∧ (p R_ b)), and SX(R_, R_, y) = ∃ p (y R_  p ∧ (p R_ y)). These queries ask if the given ABox implies that the relations R_ and R_ are the local inverses of each other in some object b or feature y appearing in the given ABox. 


Note that for any LE-𝒜ℒ𝒞 ABox 𝒜,

1. 𝒜∃ p (b R_  p ∧ (p R_ b))  iff 𝒜∪{∀ p(b R_  p  ⇒  p R_ b)} is consistent, and 

2. 𝒜∃ p (y R_  p ∧ (p R_ y))  iff 𝒜∪{∀ p (y R_  p ⇒  p R_ y)} is consistent. 

Therefore, a separation query SA(R_, R_, b) (resp. SX(R_, R_, y)) can be answered by checking if 𝒜 is consistent in the extension of LE-𝒜ℒ𝒞  with the axiom ∀ p(b R_  p  ⇒  p R_ b) (resp. ∀ p (y R_  p ⇒  p R_ y)). To this end, we consider the expansion of the LE-𝒜ℒ𝒞 tableaux algorithm with the following rules 


b R_ y
SA(R_, R_, b)
y R_ b
      
y R_ b
SX(R_, R_, y)
b R_ y
. 





The tableaux algorithm obtained by adding rule SA(R_, R_, b) (resp. SX(R_, R_, y)) to LE-𝒜ℒ𝒞 tableaux expansion rules provides a polynomial-time  sound and complete decision procedure for checking consistency of 𝒜∪{∀ p(b R_  p  ⇒  p R_ b)}(resp. 𝒜∪{∀ p (y R_  p ⇒  p R_ y)}). 


See Appendix <ref>. 


We can similarly answer the queries of the forms  SA(R_, I, b) = ∃ p (b R_  p ∧ (b I p)), and SX( R_, I, y) = ∃ p (y R_  p ∧ (p I y)) using tableaux algorithm expanded with the rules


b R_ y

b I y
    and     
y R_ b

b I y
.




However, this does not apply to all separation queries on relations. For example, consider queries of the form SA(I, R_, b) = ∃ p (b I  p ∧ (b R_ p)), and SX(I, R_, y) = ∃ p (p I y ∧ (y R_  p)). This is because the expansion of LE-𝒜ℒ𝒞 tableaux algorithm with the rules 


b I y

b R_ y
    and    b I y

y R_ b



may not be terminating. We leave this as part of future work.




§ EXAMPLES

In this section, we give a toy example of an LE-𝒜ℒ𝒞 knowledge base and some  queries of different types to demonstrate  working of various algorithms for  answering these queries discussed in the paper.

Suppose, we want to create a knowledge base to represent categorization of some movies on a streaming website  which can be used to answer some queries based on them.  We list the concept names and individual names for objects and features appearing in the knowledge base in the following tables:



    concept name     symbol     
        concept name     symbol     
        concept name     symbol 

        Italian movies     IM     German movies     GM     French movies     FM
  European movies     EUM     Recent movies     RM      Recent drama movies     RDM 
  Drama movies     DM      Famous drama movies     FDM       

        
    




     object     symbol     
         object     symbol
 
         All the President's Men     m_1     Spirited Away     m_2 
 Oppenheimer     m_3
        Cinema Paradiso      m_4 

    

 
    feature     symbol     feature     symbol      feature     symbol  

        German language      f_1      French language      f_2     Based on real story     f_3  
  Serious plot     f_4      Released after 2015     f_5     Released after 2020     f_6 

          
           
Suppose  the following  knowledge base 𝒦_1 presents the information obtained by  the website  regarding the movies, their features and their categorization into above categories from some initial source which possibly has incomplete information. 


2

    𝒜_1={    m_4:IM, (m_4 I x_∅), x_∅ :: FM∧ IM,
        x_∅::GM∧ IM, f_1::GM, f_2::FM,  
        f_4::DM, m_3:RDM, m_3 I f_6, m_1 I f_3, 
       (m_1 I f_2), (m_2:EUM)},




    𝒯_1={EUM   ≡ GM∨ FM,
    
        RDM   ≡ RM∧ DM, 
     IM   ⊑ EUM}.



For any movie m and feature y, we have m I y (resp. (m I y)) iff according to the initial source database, movie m has (resp. does not have) feature y. The feature x_∅ intuitively represents a contradiction. The terms x_∅:: FM∧ IM and x_∅:: GM∧ IM  states that there is no movie that is both a French movie and Italian movie or both a German and Italian movie. The term m_4:IM specifies that Cinema Paradiso is an Italian movie. The term f_3::AM states that Action movies have action sequences. Other terms in 𝒜_1 can be explained similarly. The term EUM≡ GM∨ FM states that the category of European movies is the smallest category on the website which contains both German movies and French movies. The term IM⊑ EUM can be equivalently written as IM≡ EUM∧ C for some new category C, meaning  all Italian movies are European movies. Other terms in 𝒯_1 can be explained similarly. Note that the terms (m_4 I x_∅), x_∅ :: FM∧ IM, and  x_∅::GM∧ IM together imply that m_4 is not in (FM∧ IM)∨(GM∧ IM). However, m_4 is in IM = EUM∧ IM = (GM∨ FM) ∧ IM. Therefore, this knowledge base is inconsistent in distributive logic but it is consistent in our setting of LE-𝒜ℒ𝒞.

 Additionally, the website also tries to get an understanding of  subjective (epistemic) view  of different user groups  on the website regarding movies, their features, and categorization.  To this end, website asks some  users from different groups the following two questions:
 
 (a) Given a list of movies:
 
 (a1) Please choose movies which have feature y from the list; 
 
 (a2) please choose movies which do not have feature y from the list.
 
 (b) Given a list of features:
 
  (b1) please choose features that describe movie m from the list;
 
 (b2) please choose features which do not describe movie m from the list. 
 
 Note that there can be movies (resp. features) in the list of options which are not chosen as answer to either (a1) or (a2) (resp. (b1) or (b2)). 
 
 We model information  obtained from above questions as follows: If some user from group i chooses movie m (resp. movie m, resp. feature y, resp. feature y) as an answer  to question (a1) (resp. (a2), resp. (b1), resp. (b2)), then we add  m R__i y (resp. (m R__i y), resp. y R__i m, resp. (y R__i m)) to the knowledge base. Note that, in general,  none of the terms y R__i m, and  m R__i y implies  other. This is because question (a) and question (b) may be asked to different users from group i.
 
 Then, for any category C, [R__i] C denotes the category defined by objects which are reported to have  all the features in C (description of C) by some user in group i. Thus, [R__i] C can be seen as the category of movies which are considered to be in C according to the user group i. This means that for any movie m in [R__i] C and any feature y of C, some user in the group i will name m as a movie having feature y as an answer to (a1).
 
 Similarly, ⟨R__i⟩ C denotes the  category defined by  features  which all objects in C (objects in C) are reported to have by some user in group i. Thus, ⟨R__i⟩ C can be seen as the category of movies defined by features which are considered to be in the description of C according to the user group i. This means that  for any feature y of ⟨R__i⟩ C and any movie m in C, some user in the group i will name y as a feature of the movie m as an answer to (b1).

 Moreover, the website can also  ask users the following questions:
 
 (c) Please choose movies which belong to the category C from a given list of movies. 
 
 (d) Please choose features that describe the category C from a given list of features.
 
 If m (resp. y) is chosen as an answer of (c) (resp. (d)) by some user in group i, then we add term m:[R__i] C (resp. y::⟨R__i⟩ C) to the knowledge base. Here, we assume that for any feature y in description of C, if some user chooses m as a movie in category C, then there is some user from the same group who will also choose m as a movie with feature y in answer to (a1). This assumption ensures that the [R__i] C is interpreted  in  accordance with LE-𝒜ℒ𝒞 semantics from relation R__i.
 
 Similarly,  for any movie m in C,  we assume that if some user chooses y as a feature in category C, then there is some user from the same group will also choose y as a feature with movie m in answer to (b1). 
  This assumption ensures that the  ⟨R__i⟩ C  is interpreted  in  accordance with LE-𝒜ℒ𝒞 semantics from relation R__i [These assumptions can be justified if we assume we have a large number of users in each group so that at least some users in the group will have the information regarding all the movies and their features under consideration.].
 
 
 
 

 
     
     
    
     



The following table presents knowledge  base 𝒦_2  representing different user groups' views regarding the movies obtained from the answers to the above questions. For simplictiy, we assume that we have only two different user groups. From here on, we will use _i (resp. _i) to denote [R__i] (resp. ⟨R__i ⟩) for i=1,2.

2

    𝒜_2={    m_3 R__1 f_3, m_3 R__2 f_3,(m_1 R__1 f_6),
        f_3 R__1 m_3, f_3 R__2 m_3, m_3: _2 RDM, 
        f_5::_1 RM, (m_1 R__2 f_5)},




    𝒯_2={FDM    ≡_1 DM ∧_2 DM}.


Let 𝒦 =𝒦_1 ∪𝒦_2
be the knowledge base obtained by combining knowledge from the source database and from users.
Given the knowledge base 𝒦, we can answer the following queries.


Positive queries.
By Lemma <ref>, these queries can be answered using the universal model constructed using the Tableaux Algorithm <ref> from the ABox obtained by unraveling 𝒦. We depict this model in Appendix <ref>.  

(1) q(p)=m_3 I p asking to name all the features implied by 𝒦 that the movie Oppenheimer has. Using the universal model, we can give the answer q(a)={f_4,f_6}.

(2) q=m_4:FDM asking if 𝒦 implies that Cinema Paradiso is a Famous drama movie. We can give  answer `No' since in the universal model, I(m_4, x_FDM)=0. 

(3) q=_2 RDM ⊑_2 DM asking if 𝒦 implies that all the movies considered to be recent drama movies by users in group 2 are also considered to be drama movies by them. We can give  answer `Yes' since in the universal model, a__2 RDM I x__2 DM.

(4) q=m_3:_2_1 RM asking if 𝒦 implies whether for any feature which is considered to be in the description of Recent movies according to some user in group 1, there is some user in group 2 who considers (reports) Oppenheimer to have this feature. We can give answer `No' since in the universal model of the knowledge base  𝒦'= 𝒦∪{a__2_1 RM: _2_1 RM, x__2_1 RM:: _2_1 RM, I(m_3, x__2_1 RM)=0.  In Appendix <ref>, we provide the universal model for 𝒦  which is obtained from  complete tableaux expansion  of 𝒦. It is easy to check from the shape of the tableaux expansion rules  that no tableaux expansion rule can add term m_3 I x__2_1 RM during the expansion of knowledge base 𝒦'. Hence, 
I(m_3, x__2_1 RM)=0 holds in the universal model of 𝒦'. 


Negative queries.
(1) q=(m_1:_2_1 RM) asking if 𝒦 implies that the movie All the President's Men is not a movie in category _2_1 RM (interpretation of this category is mentioned in previous example). We can give the answer `Yes' since, if we add the term m_1:_2_1 RM to 𝒦, this term along with the term f_5::_1 RM appearing in 𝒦, we would get m_1 R__2 f_5 by rule . Thus, the resulting knowledge base is not consistent, which means that 𝒦 implies (m_1:_2_1 RM). 

(2) q=(m_3 R__1 f_4) asking if 𝒦 implies that some user in group 1 considers Oppenheimer to be a movie which does not have a serious plot. We can give the answer `No' since the ABox obtained by  unraveling 𝒦 does not contain the term (m_3 R__1 f_4) and by Lemma <ref> it is not implied by 𝒦. 

Separation queries.
(1) q= Dif(m_2, m_4) asking if 𝒦 implies that there is a feature that one of the movies Spirited Away and Cinema Paradiso has but the other does not. We can give the answer `Yes'. If we add the rules SA(m_2,m_4) and SA(m_4,m_2) to the LE-𝒜ℒ𝒞 tableaux expansion rules and run the resulting tableaux algorithm on ABox obtained by unraveling 𝒦, we will get the clash as showed below. 



rules      premises      added terms  

   create         x_GM∨ FM:: GM∨ FM

    ∧_A     m_4:(GM∨ FM)∧ C     m_4:GM∨ FM, m_4:C 

    I     m_4:GM∨ FM,  x_GM∨ FM:: GM∨ FM      m_4 I x_GM∨ FM

    SA(m_4,m_2)      m_4 I x_GM∨ FM     m_2 I x_GM∨ FM 

    x     (m_2:GM∨ FM)     (m_2 I x_GM∨ FM) 

    



(2) q=SA(R__1, I, m_4) asking if 𝒦 implies that there is a feature that some user in group 1 considers Cinema Paradiso has but according to the initial source database it does not. We can give the answer `No', since if we add the rule SA(R__1, I, m_4) to the LE-𝒜ℒ𝒞 tableaux expansion rules and run the resulting tableaux algorithm on ABox obtained by unraveling 𝒦, we will get no clash, i.e. 𝒦 is consistent in the extension of LE-𝒜ℒ𝒞 with the axioms ∀ y (m_4 R__1 y ⇒ m_4 I y).

a small example to show how non-distributivity makes difference.

The example seems very "flat", which doesn't play on the usual strengths of DLs, i.e. when relational restrictions can be nested in each other. Here, there are basically two relations, I and R_, but they are not used in a nested way. The TBox also does not contain any relations at all.

 
Let us consider a knowledge base regarding categorization of actors and epistemic understanding of these categories according to some epistemic agent. We list the concept names and individual names for objects and features appearing in the knowledge base in the following tables:







The interpretations of the notations are given as follows. For any object a and feature x appearing in 𝒦, a I x if a has the feature x. Let R_ be a relation corresponding to an epistemic agent i defined as: for any object a and feature x, a R_ x if a has the feature x according to the agent i. For any concept C, [R_] C denotes the epistemic interpretation of C, that is, the formal concept generated by the set of objects which have all the features of C according to some agent i.

We give a knowledge base 𝒦=(𝒜, 𝒯), where 





TBox term VDA ≡ (D ∧ M) ∨ (D ∧ TV) states that the versatile actor category is the smallest category (in categorization described by 𝒦) containing the category of actors who are both drama and movie actors and the category of actors who are both drama and TV actors. ABox term (s R_ r) states that “according to some agent, Stephen Chow is not acting in some main or supporting role”, j:[R_] F states that “according to some agent, Jean-Paul Belmondo is a French actor”, and (m:M) states that “Michael Jordan is not a movie actor”. We can similarly explain the intuitive meaning of  other ABox and TBox terms. 

 





§ CONCLUSION AND FUTURE WORK


In this paper, we have shown that the tableaux algorithm for LE-𝒜ℒ𝒞, or its extension with appropriate rules, can be used to answer several types of queries over LE-𝒜ℒ𝒞 ABoxes in polynomial time. Additionally, can  generalize  these algorithms to exponential time algorithms for  LE-𝒜ℒ𝒞  knowledge bases with acyclic TBoxes by unraveling. 



Dealing with cyclic TBoxes and  RBox axioms. 
In this paper, we introduced a tableaux algorithm only for knowledge bases with acyclic TBoxes. In the future, we intend to generalize the algorithm to deal with cyclic TBoxes as well. Another interesting avenue of research is to  develop  tableaux and query answering algorithms  for  extensions of  LE-𝒜ℒ𝒞 with RBox axioms. RBox axioms are used in  description logics to describe the relationship between different relations in  knowledge bases and  the properties of these relations such as reflexivity, symmetry, and transitivity.  It would be interesting to see if it is possible to obtain necessary and/or sufficient conditions on the shape of RBox axioms for which a tableaux algorithm can be obtained. This has an interesting relationship with the problem in LE-logic of providing computationally efficient proof systems for various extensions of LE-logic in a modular manner <cit.>. 

Universal models for other types of queries
In this work, we showed that the  model constructed from tableaux Algorithm <ref> acts as universal model for several types of positive queries. In the future, it would be interesting to study if we can develop tableaux algorithms in such way that the resulting models can act as universal models for negative queries and other types of queries. This would allow the algorithm to answer multiple such queries efficiently. 

Answering more types of queries
In Section  <ref>, we mentioned that  certain separation queries cannot be answered by our method due to potential non-termination of tableaux arising from the naive extension LE-𝒜ℒ𝒞 tableaux expansion rules corresponding to these queries. However, it may be possible to achieve termination in some of these case  by incorporating appropriate loop check conditions into these expansion rules. In the future, we intend to study such extensions. 

Generalizing to more expressive description logics. The  DL LE-𝒜ℒ𝒞 is the non-distributive counterpart  of  𝒜ℒ𝒞. A natural direction for further research is to explore the non-distributive counterparts of extensions of 𝒜ℒ𝒞 such as  𝒜ℒ𝒞ℐ and 𝒜ℒ𝒞ℐ𝒩 and fuzzy generalizations of such description logics. 
This would allow us to express more constructions like concepts generated by an object or a feature, which can not be expressed in LE-𝒜ℒ𝒞. This would provide us language to answer many more types of interesting queries regarding enriched formal contexts. 


eptcs





§ PROOFS

In this section, we collect proofs of some results  stated throughout the paper.



 §.§ Proof of Theorem <ref>

In this part, we will prove the termination, soundness and completeness of tableaux algorithms for checking consistency of 𝒜∪{∀ p (b I p ⇒ d I p)}  and  𝒜∪{∀ p (p I y ⇒ p I z)} defined in Section <ref>. We only give the proof for 𝒜∪∀ p (b I p ⇒ d I p), the proof for 𝒜∪∀ p (p I y ⇒ p I z) would be similar. 


In this paper, we will only explain the changes that must be made to the termination, soundness, and completeness proofs of the LE-𝒜ℒ𝒞 tableaux algorithm provided in <cit.>. We refer to <cit.> for details of these proofs.

Termination. To prove termination, we prove that the following lemma proved for LE-𝒜ℒ𝒞 tableaux algorithm in <cit.> also holds for its extension with rule SA(b,d). 


 <cit.>
For any individual names b, and y, and concept C  added during tableau expansion of 𝒜, 

    _𝒟(C) ≤_𝒟(𝒜)+1   _𝒟(C) ≤_𝒟(𝒜)+1,



    -_𝒟(𝒜 )-1 ≤_𝒟 (b)   _𝒟(b) ≤_𝒟(𝒜)+1,



    -_𝒟(𝒜)-1 ≤_𝒟(y)  _𝒟(y) ≤_𝒟(𝒜)+1



 The proof proceeds by showing that the following stronger claim holds. For any tableaux expansion  𝒜, obtained from 𝒜 after any finite number of expansion steps:

1. For any term b I y ∈𝒜, _𝒟 (b) -  _𝒟 (y) ≤_𝒟(𝒜)+1, and _𝒟 (y) -  _𝒟 (b) ≤_𝒟(𝒜)+1.


2. For any term b R_ y ∈𝒜, _𝒟 (b) +1 -  _𝒟 (y) ≤_𝒟(𝒜)+1, and _𝒟 (y) -  _𝒟 (b) ≤_𝒟(𝒜)+1.

3. For any term y R_ b ∈𝒜, _𝒟 (b) -  _𝒟 (y) ≤_𝒟(𝒜)+1, and _𝒟 (y) +1  -  _𝒟 (b) ≤_𝒟(𝒜)+1.

4. For any term b:C ∈𝒜, _𝒟 (b)  +  _𝒟 (C) ≤_𝒟(𝒜)+1, and -_𝒟 (b) -  _𝒟 (C) ≤ 0.

5. For any term y::C ∈𝒜, -_𝒟 (y)  - _𝒟 (C) ≤ 0, and _𝒟 (y) +  _𝒟 (C) ≤_𝒟(𝒜)+1.

The proof proceeds by induction of number of rules applied. The proofs for initial case (i.e. for all the terms in original ABox 𝒜) and all the LE-𝒜ℒ𝒞  tableaux expansion rule are provided in <cit.>. Therefore, to complete the proof we need to show that the rule  SA(b,d) also preserves these properties. Suppose a term d I y is added from a term b I y using rule SA(b,d). In this case, by induction, we have _𝒟 (b) -  _𝒟 (y) ≤_𝒟(𝒜)+1, and _𝒟 (y) -  _𝒟 (b) ≤_𝒟(𝒜)+1. As b and d are object names appearing in 𝒜, we have _𝒟 (b) = _𝒟 (d)=_𝒟 (b) = _𝒟 (d)=0. Therefore, we have _𝒟 (d) -  _𝒟 (y) ≤_𝒟(𝒜)+1, and _𝒟 (y) -  _𝒟 (d) ≤_𝒟(𝒜)+1. Hence proved.


This lemma bounds the number of new contestant and concept names that can appear in tableaux expansion. Therefore, it implies that the number of  terms that can appear in tableaux expansion are bounded by poly(size(𝒜)). As tableaux has no branching rules, this implies termination. (See <cit.> for more details).



  
Soundness. The soundness follows immediately from the soundness for LE-𝒜ℒ𝒞 tableaux algorithm <cit.>, and the fact that  the rule SA(b,d) ensures that the model obtained from completion satisfies the axiom ∀ p (b I p ⇒ d I p).



  
Completeness. To prove completeness, we show that the following lemma proved for LE-𝒜ℒ𝒞 <cit.> also holds for its extension with the axiom ∀ p (b I p ⇒ d I p). 


For any ABox 𝒜,  any model M=(𝔽, ·^ℳ) of 𝒜 can be extended to a model M'=(𝔽', ·^ℳ') such that 𝔽'=(A',X',I',{R_'}_∈𝒢, {R_'}_∈ℱ), A ⊆ A' and X ⊆  X', and moreover for every ∈𝒢 and ∈ℱ:

1. There exists a_C ∈ A' and x_C ∈ X'  such that:

    C^ℳ' =(I'^(0)[x_C^ℳ'], I'^(1)[a_C^ℳ']),    a_C^ℳ'∈C^ℳ',     x_C^ℳ'∈C^ℳ',


 2. For every individual b in A there exist b and b in A' such that:

    I'^(1)[ b] = R_'^(1)[b^ℳ']      I'^(1)[ b] = R_'^(0)[b^ℳ'],


3. For every individual y in X there exist y and ▪ y in X' such that:

    I'^(0)[▪ y] = R_'^(1)[y^ℳ']      I'^(0)[ y] = R_'^(0)[y^ℳ'].


4. For any C, C^ℳ= C^ℳ'∩ A and C^ℳ= C^ℳ'∩ X. 

In <cit.>, this lemma was proved by constructing such model M'.  Here, we show that if the model M additionally satisfies axiom ∀ p (b I p ⇒ d I p), then so does the model M'. This follows from the fact that the model M' is constructed in such a way that (see <cit.> for more details) for any b,d ∈ A, a term b I^ℳ' x_C is added for some newly added element x_C∈ X'∖ X iff we have b I^ℳ y for all y ∈ C^ℳ. Then, as M ∀ p (b I p ⇒ d I p), we also get d I y for all y ∈ C^ℳ  which implies d I^ℳ' x_C. 

The above lemma ensures that if 𝒜∪{∀ p (b I p ⇒ d I p)}  has a model, then it has a model with classification of objects and features. The completeness proof then proceeds by showing that if 𝒜 is consistent, then the model for 𝒜 with the above properties satisfies all the terms in the completion of 𝒜. We refer to <cit.> for details.




 §.§ Proof of Theorem <ref>

We only give the proof for SA(R_, R_, b). The proof for SX(R_, R_, y) is similar. The proof for soundness and completeness is analogous to the proof for soundness and completeness of Theorem <ref> given in Section <ref>. 
To prove termination, we would need the following lemma.


We define -leading concepts as the smallest set of concepts  satisfying the following conditions. 

    
  * For any atomic concept C, the concept C is -leading.
    
  * If C is  -leading, then  C is  -leading.
    
  * If C is   -leading, then C∨ C_1 is    -leading for any C_1. 
      
  * If C_1 and C_2 are  -leading, then C_1 ∧  C_2 is  -leading. 
 
We define -leading concepts as the smallest set of concepts  satisfying the following conditions.

    
  * For any atomic concept C, the concept C is -leading.
    
  * If C is  -leading, then  C is  -leading.
    
  * If C is   -leading, then C∧  C_1 is    -leading for any C_1. 
    
  * If C_1 and C_2 are  -leading, then C_1 ∨  C_2 is  -leading. 
 

Note that a concept C_1 ∧ C_2 (resp. C_1 ∨ C_2) is -leading (resp. -leading) iff both C_1 and C_2 are -leading (resp. -leading). 

 

For any LE-𝒜ℒ𝒞 ABox 𝒜 and any individual names b, y, the following holds:


  * If a term of the form  b I x_C or  b :C or x_C R_ b or  b I ▪ x_C appears in 𝒜, then C must be -leading. 


  * If a term of the form  a_C I  y or  y::C or a_C R_  y or a_C I y appears in 𝒜, then C must be -leading. 


  * If we have a term of the form x_C::C' or a_C' I x_C or a_C':C in 𝒜,  and C is -leading, then  C' is also -leading. 


  * If we have a term of the form a_C:C' or a_C I x_C' or x_C'::C in 𝒜,  and C is -leading, then  C' is also -leading. 
    
  * No term of the form b I  y 
can belong to 𝒜. 
    
  * No term of the form b R_ y    
    can belong to 𝒜. 
    
  * No constant of the form b or ▪ y appears in 𝒜 for any b or y. 





The proof follows by a simultaneous induction on the number of applications of the expansion rules. The proof for base case is obvious as 𝒜 does not contain individual name of the form b or y. We give the proof for all inductive cases now.

Creation rule: Only terms added by this rule are of the form a_C:C or x_C::C for some C ∈𝒜. For terms of both of these types,  all the items in lemma hold trivially.  

Basic rule: In this case, we add term b I y from terms b:C and y::C. We only need to consider the following cases: (1) b is of the form d, and y is of the form x_C' for some C'. By induction item 1, C is -leading. 
Hence, by induction item 4, C' is also -leading. Therefore, the new term 
d I x_C' also satisfies item 1. (2) b is of the form a_C' for some C', and y is of the form z. By induction item 2, C is -leading. Hence, by induction item 3, C' is also -leading. Therefore, the new term  a_C' I  z also satisfies item 2.  (3) b is of the form a_C_1, and y is of the form x_C_2. In this case, if C_1 (resp. C_2) is -leading (resp. -leading), then by induction item 4 (resp. item 3) C would be be -leading (resp. -leading). 
By again applying the same items, we would get C_2 (resp. C_1) is -leading (resp. -leading). Therefore, the added term a_C_1 I x_C_2 satisfies items 3 and 4. Item 5 is satisfied, since if any of these terms is of the form b I  y, then both b:C, and y::C appear in 𝒜. By induction items 1 and 2 C must be both -leading and  -leading. However, no such concept exists. Item 7  is satisfied as this rule does not add new individual names.

 

Rules ∧_A and ∨_X: We only give the proof for ∧_A, the proof for ∨_X is dual. In this case, we add terms b:C_1, and b:C_2 from term b:C_1 ∧ C_2. We need to consider the following cases: (1) b is of form d. By induction item 1, C_1 ∧ C_2 is -leading. Therefore, both C_1 and C_2 must be -leading. Hence, the newly added terms b:C_1 and b:C_2 also satisfy item 1. (2) b is of the form a_C. We have to show items 3 and 4 hold. If C is -leading, then by induction item 4, C_1 ∧ C_2 is -leading, which implies that both C_1 and C_2 are -leading. Hence, the added terms b:C_1 and b:C_2 satisfy item 4. To show item 3 holds for the new  terms,  w.l.o.g. suppose C_1 is -leading. Then, by def. C_1 ∧ C_2 is -leading as well. Therefore, by induction item 3, C is -leading. We can similarly show  C is -leading, when C_2 is -leading.   Item 7  is satisfied as this rule does not add new individual names.


Rules  and :  We only give the proof for , the proof for  is dual. In this case, we add term of the form b R_ y from terms b:[R_]C and y::C.  By induction item 6, b can not be of the form d. If b is of the form a_C' for some C', then by induction item 3, C' is -leading. Hence, the added term a_C' R_ y satisfies item 2. It also satisfies item 6 because C' being -leading can not have  as the outermost connective.  Item 7  is satisfied as this rule does not add new individual names.

Rules y, ▪ y, b, and b:  We only give the proof for y, the proofs for other rules are similar. In this case, we add term of the form b R_ y from term b I  y. By induction item 6, b can not be of the form d. If b is of the form a_C for some C, then by induction item 2, C must be -leading. Therefore, the added term a_C R_ y satisfies item 2. It also satisfies item 6, since  C being -leading, can not have  as the outermost connective.  Item 7  is satisfied as this rule does not add new individual names.


Rules ∧_A^-1 and ∨_X^-1:  We only give the proof for ∧_A^-1, the proof for ∨_X^-1 is dual. In this case, we add term of the form b:C_1 ∧ C_2 from terms of the form b:C_1 and b:C_2. We need to consider the following cases: (1) 
b is of the form d, then by induction item 1, C_1 and C_2 are -leading. Then, by def. C_1 ∧ C_2 is also -leading. Therefore, the new term b:C_1 ∧ C_2 satisfies item 1. (2) b is of the form a_C. We have to show items 3 and 4 hold. If C is -leading, then by induction item 4, both C_1 and C_2 are -leading, which implies that C_1 ∧ C_2 is -leading. Hence, new term b:C_1 ∧ C_2 satisfies item 4. To show item 3 holds for the new  term, suppose C_1 ∧ C_2 is -leading. Then, C_1 is -leading or C_2 is -leading. Therefore, by induction item 3, C is -leading. It also satisfies item 6, since C being -leading, can not have  as the outermost connective.   Item 7  is satisfied as this rule does not add new individual names.

Rules R_ and  R_: We only the give proof for R_, the proof for R_ is dual. In this case, we add terms b I  y, and b I y from b R_ y. 
By induction item 5, b can not be of the form d. If b is of the form a_C for some C, then by induction item 2, C must be -leading. Therefore, the added terms a_C I  y and a_C I y satisfy item 2. As  b can not be of the form d, the possibly  new constant b is not of the form d for any d. Hence, item 3 is satisfied. 

Rules a_C and x_C:  We only give the proof for a_C, the proof for x_C is dual. In this case, we add term of the form b:C from term b I x_C. We need to consider the following cases: (1) b is of the form d, then by induction item 1, C must be -leading. Therefore, the added term b:C also satisfies item 1. (2) If b is of the form a_C' for some C'. We have to show items 3 and 4 hold. If C' is -leading, then by induction item 4, C is -leading. Hence, added term a_C':C satisfies item 4. To show item 3 holds for the new  term, w.l.o.g. suppose C is -leading. Then, by induction item 3, C' is -leading. 


As a corollary, we get the following result.


  For any LE-𝒜ℒ𝒞 ABox 𝒜, and any terms d R_ z, and y R_ b, if  dR_ z ∈𝒜∪{y R_ b}, then  d R_ z ∈𝒜.  


For any term of the form y R_ b, the only rule that has it in premise is the adjunction rule R_ which adds terms b I y, and b I ▪ y. The term b I ▪ y cannot lead to the addition of any other term. If the term b I y leads to the addition of a term of the form d R_ y, then it means that we must have b : C ∈𝒜, for some C or b I  z ∈𝒜  for some z. However, none of these is possible by the lemma <ref>. 


This lemma immediately implies the following modified version of Lemma <ref>. 

 
For any individual names b, and y, and concept C  added during tableau expansion of 𝒜, 

    _𝒟(C) ≤_𝒟(𝒜)+1   _𝒟(C) ≤_𝒟(𝒜)+1,



    -_𝒟(𝒜 )-2 ≤_𝒟 (b)   _𝒟(b) ≤_𝒟(𝒜)+1,



    -_𝒟(𝒜)-1 ≤_𝒟(y)  _𝒟(y) ≤_𝒟(𝒜)+2




The proof proceeds by showing that the following stronger claim holds. For any tableaux expansion 𝒜, obtained from 𝒜 after any finite number of expansion steps:

1. For any term b I y ∈𝒜, _𝒟 (b) -  _𝒟 (y) ≤_𝒟(𝒜)+1, and _𝒟 (y) -  _𝒟 (b) ≤_𝒟(𝒜)+2.


2. For any term b R_ y ∈𝒜, _𝒟 (b) +1 -  _𝒟 (y) ≤_𝒟(𝒜)+1, and _𝒟 (y) -  _𝒟 (b) ≤_𝒟(𝒜)+1.

3. For any term y R_ b ∈𝒜, _𝒟 (b) -  _𝒟 (y) ≤_𝒟(𝒜)+1, and _𝒟 (y) +1  -  _𝒟 (b) ≤_𝒟(𝒜)+2.

4. For any term b:C ∈𝒜, _𝒟 (b)  +  _𝒟 (C) ≤_𝒟(𝒜)+1, and -_𝒟 (b) -  _𝒟 (C) ≤ 1.

5. For any term y::C ∈𝒜, -_𝒟 (y)  - _𝒟 (C) ≤ 0, and _𝒟 (y) +  _𝒟 (C) ≤_𝒟(𝒜)+1.

The proof relies on the idea that the new rule  SA(R_, R_, b)  introduces a new term of the form y R_ b from a term b R_ y. However, by Corollary <ref>
the term  b R_ y  must belong to the LE-𝒜ℒ𝒞 completion of 𝒜. Hence, it satisfies Condition 2 by Lemma <ref>. The proof for all other conditions follows by a straightforward generalization of the proof of <cit.>. 





§ MODELS FOR EXAMPLE KNOWLEDGE BASE
 
The knowledge base in Section <ref> is given by 𝒦 =𝒦_1 ∪𝒦_2, where the initial source database 𝒦_1=(𝒜_1,𝒯_1) is given by

2


    𝒜_1={    m_4:IM, (m_4 I x_∅), x_∅ :: FM∧ IM,
        x_∅::GM∧ IM, f_1::GM, f_2::FM,  
        f_4::DM, m_3:RDM, m_3 I f_6, m_1 I f_3, 
       (m_1 I f_2), (m_2:EUM)},




    𝒯_1={EUM   ≡ GM∨ FM,
    
        RDM   ≡ RM∧ DM, 
     IM   ⊑ EUM},




while the database from users of two different groups 𝒦_2 = (𝒜_2,𝒯_2) is given by

2

    𝒜_2={    m_3 R__1 f_3, m_3 R__2 f_3,(m_1 R__1 f_6),
        f_3 R__1 m_3, f_3 R__2 m_3, m_3: _2 RDM, 
        f_5::_1 RM, (m_1 R__2 f_5)},




    𝒯_2={FDM    ≡_1 DM ∧_2 DM}.




By unraveling TBoxes we get the following terms:

    
  * EUM≡ GM∨ FM
    
  * RDM≡ RM∧ DM
    
  * IM≡ (GM∨ FM)∧ C for some C not appearing in 𝒦
    
  * FDM ≡_1 DM ∧_2 DM


Note that the terms FM∧ IM and GM∧ IM in 𝒜_1 are denoted as follows.

    
  * FM∧ IM≡ FM∧ ((GM∨ FM)∧ C)≡ FM∧ C
    
  * GM∧ IM≡ GM∧ ((GM∨ FM)∧ C)≡ GM∧ C


 

   
   
   
   


We denote the objects and features in the model  of the form a_C, and x_C as below:



a_1      a_GM      x_1      x_GM

a_2      a_FM      x_2      x_FM 

a_3      a_GM∨ FM     x_3     x_GM∨ FM  

a_4      a_RM        x_4      x_RM

a_5      a_DM        x_5      x_DM 

a_6      a_RM∧ DM     x_6      x_RM∧ DM  

a_7     a_C     x_7     x_C

a_8     a_(GM∨ FM)∧ C     x_8     x_(GM∨ FM)∧ C

a_9     a_FM∧ C     x_9     x_FM∧ C

a_10      a_GM∧ C        x_10      x_GM∧ C

a_11      a__1 DM        x_11      x__1 DM

a_12      a__2 DM        x_12      x__2 DM

a_13     a__1 DM∧_2 DM     x_13     x__1 DM∧_2 DM

a_14     a__2 (RM∧ DM)        x_14      x__2 (RM∧ DM)

a_15      a__1 RM        x_15      x__1 RM

a_16      a_⊤        x_16      x_
 
          x_17     x_∅





We give the following table depicting all the objects and features appearing in the model and whether or not they are related by I.  







The relations R__i, and R__i are given as follows. We have  R__1 = {(a_11,x_5), (a_13, x_5), (m_3,f_3))}, and R__2 = {(a_12,x_5), (a_13, x_5), (a_14, x_4), (a_14, x_5), (a_14, x_6),(a_14,f_4),(m_3,x_4), (m_3,x_5), (m_3,x_6), (m_3,f_3),(m_3,f_4)}. R__1 = {(f_5,a_4),(f_5,a_6),(f_3,m_3),(f_5,m_3),(x_15,a_6),(x_15,a_4),(x_15,m_3)} and R__2 = {(f_3,m_3)}. The model contains atomic concepts GM, FM,  RM, DM, and C. For any of these concepts D, its interpretation is given  by the tuple (x_D^↓, a_D^↑).


Figure <ref> depicts the concept lattice generated by the formal context defining the model with the help of lattice visualization by LatViz <cit.>.  




a_6-x_5 proof 


    Rule     Premise     added term 

    create      a_M ∧ C_1:M ∧ C_1      a_M ∧ C_1:M,  a_M ∧ C_1:C_1
 
    create          x_M ∨ TV:: M ∨ TV 

    ∨     x_M ∨ TV:: M ∨ TV     x_M ∨ TV::M, x_M ∨ TV::TV 
 
    I     a_M ∧ C_1:M,  x_M ∨ TV::M     a_M ∧ C_1 I x_M ∨ TV

    x_C      a_M ∧ C_1 I x_M ∨ TV     a_M ∧ C_1 : M ∨ TV

    ∧^-1     a_M ∧ C_1 : M ∨ TV, a_M ∧ C_1:C_1     a_M ∧ C_1: ( M ∨ TV) ∧ C_1


a_7-x_5 is similar. 


Proof for a_8-x_3



    Rule     Premise     added term 

     create          x_M ∨ TV::M ∨ TV  
 
    ∨     x_M ∨ TV::M ∨ TV     x_M ∨ TV::M,  x_M ∨ TV::TV 

    previously done        a_M ∧ C_1:M 

    I     a_M ∧ C_1:M,  x_M ∨ TV::M     a_M ∧ C_1 I x_M ∨ TV 

    a_C     a_M ∧ C_1 I x_M ∨ TV     x_M ∨ TV:: M ∧ C_1


You can similarly show that you have term x_M ∨ TV::TV ∧ C_1, and then by ∨^-1, we would get x_M ∨ TV::(M ∧ C_1) ∨ (TV ∧ C_1) which by creation and basic rule gives a_(M ∧ C_1) ∨ (TV ∧ C_1)  I  x_M ∨ TV).  You can show other two similarly




