=Paper=
{{Paper
|id=Vol-1921/paper8
|storemode=property
|title=Application of Boolean-valued Models and FCA for the Development of Ontological Models
|pdfUrl=https://ceur-ws.org/Vol-1921/paper8.pdf
|volume=Vol-1921
|authors=Dmitry Palchunov,Gulnara Yakhyaeva
}}
==Application of Boolean-valued Models and FCA for the Development of Ontological Models==
<pdf width="1500px">https://ceur-ws.org/Vol-1921/paper8.pdf</pdf>
<pre>
    Application of Boolean-valued models and FCA for the
              development of ontological models

                          Dmitry Palchunov, Gulnara Yakhyaeva



       Abstract. The paper is devoted to the development of methods of ontology
       supported knowledge discovery in the field of mobile network subscribers. We
       develop the ontological model of the domain of mobile networks. This ontolog-
       ical model is intended to describe the behavior of mobile network subscribers.
       The ontological model is based on the four-level model of knowledge represen-
       tation. In the paper, special attention is given to the third level which represents
       the set of cases from the domain. For the analysis of domain cases and for the
       generation of fuzzy knowledge about the domain we use Boolean-valued mod-
       els, fuzzy models and Formal Concept Analysis. To describe the set of cases
       from the domain we use formal contexts; objects of these formal contexts are
       models representing sets of subscribers. We study formal contexts generated by
       Boolean-valued models, and formal concepts of these formal contexts. We ob-
       tain a description of theories of classes of domain cases in the language of for-
       mal concepts.

       Keywords: Boolean-valued model, fuzzy model theory, ontology, ontological
       model, mobile networks, mobile network subscribers, FCA, formal context,
       formal concept


1      Introduction

The article is devoted to the development of an ontological model of the domain of
mobile networks. The ontological model is based on the four-level model of
knowledge representation [1, 2]. We apply model-theoretical methods [3], theory of
fuzzy models [4] and FCA [5, 6] to construct the ontological model.
   The present investigations continue the studies begun in [7, 8]. In [8] the ontologi-
cal model of the domain of mobile networks was used to determine which tariffs and
services of the mobile operator are most interesting and useful for a given mobile
network user. In this article we expand the borders of our consideration of the do-
main. We are interested in revealing high-level characteristics of the subscriber: in-
come level, social status, mobility, interests, preferences, etc. The elucidation of high-
level characteristics is necessary to predict the behavior of the subscriber.
   Thus we need to consider not only properties of individual subscribers, but also the
interaction of subscribers (for example, calls between subscribers and so on). There-
fore, in contrast to [8], we need to consider not only unary predicates, but also binary
predicates to describe the domain ontology. A case model of this domain is represent-
ed as a set of countable algebraic systems.
   Next, in the paper we describe a method for constructing a formal context for the
case model (using the notion of a Boolean-valued model) and a method of transition-
ing to an object-clarified context.
   This work is mainly theoretical. The results of practical implementation will be de-
scribed in the next paper.


2      Ontological model of the domain of mobile networks

The ontological model of the domain of mobile networks is constructed on the basis
of the four-level model of knowledge representation [1, 2]. We call a tuple
                                  𝓞𝓜 = 〈𝐾, 𝜎, 𝑇 𝑎 , 𝑇 𝑠 , 𝑇𝑓 〉
an ontological model of the domain. Here 𝐾 is the set of cases of the domain, 𝜎 is the
signature of the domain, 𝑇 𝑎 is the analytic theory of the domain, 𝑇 𝑠 is the theory of
the domain and 𝑇𝑓 is the fuzzy theory of the domain.
  The first step of the construction of the ontological model is the description of the
ontology of the domain. From the model-theoretical point of view, the construction of
the domain ontology consists of describing a signature σ (i.e. the set of key concepts)
and a set of axiom 𝒜𝓍𝑎 of the given domain [9, 10]. The pair 〈𝜎, 𝒜𝓍𝑎 〉 generates the
analytic theory 𝑇 𝑎 , i.e. description of sense of the key concepts of the domain, defini-
tions of used notions. The theory of the domain 𝑇 𝑠 represents general (universal)
knowledge of the domain.
        We consider six classes of concepts to determine the signature 𝜎𝕄 of the object
domain 𝕄 = “Mobile networks”:
1. 𝜎𝑃 represents individual indicators of subscribers, and contains two parts: 𝜎𝑃1 are
   traffics and 𝜎𝑃2 are accruals.
2. 𝜎𝑄 represents different tariff plans and services.
3. 𝜎𝑅 represents properties and characteristics of various tariff plans, services and op-
   tions; for example, the number of free minutes of talk, the volume of the SMS
   package, etc.
4. 𝜎𝐼 represents concepts which express different interests of subscribers.
5. 𝜎𝑆 represents concepts which express subscriber's social status.
6. 𝜎𝑇 represents concepts which express relationships and interactions between sub-
   scribers: calls / SMS / MMS of one subscriber to another and so on.

       Note that the concepts from the classes 𝜎𝑃 , 𝜎𝑄 , 𝜎𝑅 , 𝜎𝐼 , 𝜎𝑆 represent different
properties of subscribers; these concepts are formalized as unary predicates. The con-
cepts from the class 𝜎𝑇 represent relationships and interactions between subscribers;
these concepts are formalized as binary predicates.
       The presented classes of concepts have a hierarchical structure which is de-
scribed by a set of axioms “hyponym-hypernym”. For these classes of concepts we
present axioms of completeness and axioms of including. A detailed description of
these axioms is given in [8]. We present a set of axioms of irreflexivity for the class of
concepts 𝜎𝑇 . For example, for any concept 𝑄(𝑥, 𝑦) ∈ 𝜎𝑇 we formulate an axiom
¬𝑄(𝑥, 𝑥) which means that no subscriber can call to himself. This concludes the first
step of the ontological model's constructing.
        At the second step of the construction of the ontological model, we present the
set 𝒜𝓍𝑠 of general statements about the domain. The set 𝒜𝓍𝑠 is considered to be
true at the moment but may be changed at the future time. This knowledge is synthet-
ic, in contrast to the analytical knowledge presented in the ontology. The synthetic
knowledge does not follow from the meaning of the terms used in the description of
the domain. The truth value of this knowledge depends on the present state of the real
world. An example of such knowledge is the statement that a given tariff and a specif-
ic service of the mobile operator are not compatible.
        The set of all axioms 𝒜𝓍𝑎 ∪ 𝒜𝓍𝑠 generates the theory of the domain 𝑇 𝑠 , i.e.,
a set of statements which are true in the given domain. This concludes the second step
of the ontological model's constructing.
        The third step of the building the ontological model is a formalization of em-
pirical knowledge about the domain, i.e., knowledge about the concrete precedents
(cases) of the given object area. In the domain 𝕄 the set 𝐴 of subjects is the set of
various individuals and organizations using mobile network services, etc. Note that
the set of subjects 𝐴 is finite at each point of time, but it is constantly changing in
dynamics. Therefore we may consider the set 𝐴 as potentially infinite. Thus in this
paper we consider a countable set A of subjects.
        Let us consider a set 𝐴 = {𝑎1 , 𝑎2 , … } of the subjects of the domain. Each case
(instance) of the domain 𝕄 determines an algebraic system 𝔄 = ⟨𝐴, 𝜎𝕄 ⟩, i.e., defines
the signature 𝜎𝕄 on the set A.
        Further, to simplify the formalization, we will consider models 𝔄 = ⟨𝐴, 𝜎𝕄 ⟩ in
the signature (𝜎𝕄 )𝐴 , enriched by constants for all elements of the model:
                                   (𝜎𝕄 )𝐴 = 𝜎𝕄 ∪ {𝑐𝑎 | 𝑎 ∈ 𝐴}.
So, for simplicity, we denote 𝜎 = 𝜎𝕄 , 𝜎𝐴 = (𝜎𝕄 )𝐴 and 𝔄𝐴 = ⟨𝐴, 𝜎𝐴 ⟩.
        Note that not every algebraic system 𝔄 = ⟨𝐴, 𝜎𝕄 ⟩ is the case of the domain 𝕄.
We say that a model 𝔄𝐴 is a domain’s case if 𝔄𝐴 ⊨ 𝒜𝓍𝑎 ∪ 𝒜𝓍𝑠 .
        To solve different problems we may consider different sets of cases 𝐾 ⊆
𝕂(𝜎𝐴 ). For example, the set of cases 𝐾 may describe temporal "slices" of the domain,
or geolocation "slices" of the domain. Also, the set 𝐾 may be used to describe the
behavior of different groups of subscribers.
        Empirical knowledge completely depends on the selection of the set of cases
𝐾 ⊆ 𝕂(𝜎𝐴 ) of the domain and serves as a source of generating a new knowledge
about the given domain. Below we will be construct the case model of the domain
based on the selected set of cases 𝐾.
        Using the presented formalization of the case model, we can identify high-
level characteristics of mobile network subscribers and make portraits of mobile users'
segments. To do this, we generate different Boolean-valued and fuzzy models (see
Section 3) and construct corresponding formal contexts for given case models (see
Section 4).
3       Preliminaries: Boolean-valued models and fuzzy models

In the present paper a model (an algebraic system) is a tuple
𝔄 = 〈𝐴; 𝑃1 , . . . , 𝑃𝑛 , 𝑐1 , . . . , 𝑐𝑘 〉. The set |𝔄| = 𝐴 is called the universe of the model,
𝑃1 , . . . , 𝑃𝑛 are predicates defined on the set 𝐴 and 𝑐1 , . . . , 𝑐𝑘 are constants. The tuple
𝜎 = 〈 𝑃1 , . . . , 𝑃𝑛 , 𝑐1 , . . . , 𝑐𝑘 〉 is called the signature of the algebraic system 𝔄.
    A formula having no free variables is called a sentence. For a signature 𝜎 we de-
note:
                      𝑭(𝝈) ⇋ {𝝋 | 𝝋 𝐢𝐬 𝐚 𝐟𝐨𝐫𝐦𝐮𝐥𝐚 𝐨𝐟 𝐭𝐡𝐞 𝐬𝐢𝐠𝐧𝐚𝐭𝐮𝐫𝐞 𝝈},
                    𝑺(𝝈) ⇋ {𝝋 | 𝝋 𝐢𝐬 𝐚 𝐬𝐞𝐧𝐭𝐞𝐧𝐜𝐞 𝐨𝐟 𝐭𝐡𝐞 𝐬𝐢𝐠𝐧𝐚𝐭𝐮𝐫𝐞 𝝈} and
                        𝑲(𝝈) ⇋ {𝕬 | 𝕬 𝐢𝐬 𝐚 𝐦𝐨𝐝𝐞𝐥 𝐨𝐟 𝐭𝐡𝐞 𝐬𝐢𝐠𝐧𝐚𝐭𝐮𝐫𝐞 𝝈}.
    For a sentence 𝜑 ∈ 𝑆(𝜎) and a model 𝔄 ∈ 𝐾(𝜎) we denote 𝔄 ⊨ 𝜑 if the sentence
𝜑 is true in the model 𝔄.

    Definition 1 [11]. Let 𝔹 be a complete Boolean algebra and 𝜏: S(𝜎A ) → 𝔹. A
triple 𝔄𝔹 = 〈𝐴, 𝜎𝐴 , 𝜏〉 is called a Boolean-valued model if the following conditions
hold:
                       𝜏(𝜑) = ̅̅̅̅̅̅
                                 𝜏(𝜑); 𝜏(𝜑 ∨ 𝜓) = 𝜏(𝜑) ∪ 𝜏(𝜓);
                 𝜏(𝜑 & 𝜓) = 𝜏(𝜑) ∩ 𝜏(𝜓); 𝜏(𝜑 → 𝜓) = ̅̅̅̅̅̅
                                                         𝜏(𝜑) ∪ 𝜏(𝜓);
               𝜏(∀𝑥𝜑(𝑥)) = ⋂ 𝜏(𝜑(𝑐𝑎 )); 𝜏(∃𝑥𝜑(𝑥)) = ⋃ 𝜏(𝜑(𝑐𝑎 )).
                                𝑎∈𝐴                              𝑎∈𝐴


   We use the notion of a fuzzy model to formalize the estimated knowledge of the
object domain (the fourth level of the construction of the ontological model). Each
fuzzy model is a special case of the fuzzification of some Boolean-valued model [12,
13].
   Definition 2 [4]. Let 𝔄𝔹 = 〈𝐴, 𝜎A , 𝜏〉 be a Boolean-valued model, where
𝜏: S(𝜎A ) → 𝔹, and ℎ: 𝔹 → [0,1] be a mapping for which ℎ(0) = 0 and ℎ(1) = 1.
          We define a valuation 𝜇: S(𝜎A ) → [0,1] as a composition 𝜇(𝜑) = ℎ(𝜏(𝜑)).
A triple 𝔄𝜇 = ⟨𝐴, 𝜎𝐴 , 𝜇⟩ is called a fuzzification of the Boolean valued-model 𝔄𝔹 via
the mapping ℎ.

     Definition 3 [4]. The mapping ℎ: 𝔹 → [0,1] is called an additive homomorphism
if
         (1) ℎ preserves the order, i.e., ℎ is a homomorphism ℎ: 𝔹 → [0,1] of posets
             with constants 0 and 1;
         (2) ℎ is additive, i.e.,
                 𝑎 ∩ 𝑏 = 0 ⇒ ℎ(𝑎 ∪ 𝑏) = ℎ(𝑎) + ℎ(𝑏) for any 𝑎, 𝑏 ∈ 𝔹.

   Definition 4 [4]. A fuzzy model 𝔄𝜇 = ⟨𝐴, 𝜎𝐴 , 𝜇⟩ is a fuzzification of a Boolean-
valued model 𝔄𝔹 = 〈𝐴, 𝜎A , 𝜏〉 via an additive homomorphism.
4      Main results: formal contexts for Boolean-valued models

Remark 5. Let 𝔄𝔹 = 〈𝐴, 𝜎A , 𝜏〉 be a Boolean-valued model and 𝜏: S(σA ) → 𝔹. Con-
sider the formal context (𝔹, 𝑆(𝜎𝐴 ), 𝐼), where 𝑏 𝐼 𝜑 ⇔ 𝜏(𝜑) = 𝑏. Note that the non-
empty extents of formal concepts are one-element sets.




                           Fig. 1. The formal context (𝔹, 𝑆(𝜎𝐴 ), 𝐼).

   For a formal context (𝐺, 𝑀, 𝐼) by 𝔙(𝐺, 𝑀, 𝐼) we denote the lattice of formal
concepts of the formal context (𝐺, 𝑀, 𝐼).
   Definition 6 [14]. Let 𝔄𝔹 = 〈𝐴, 𝜎A , 𝜏〉 be a Boolean-valued model, where
𝜏: S(𝜎A ) → 𝔹. Consider an atom 𝑏 ∈ At(𝔹). Define a model 𝔄b ∈ 𝕂(𝜎A ) by setting
                    𝔄b ⊨ 𝑃(𝑐1 , … , 𝑐n ) ⇔ 𝑏 ≤ τ(𝑃(𝑐1 , … , 𝑐n ))
for any 𝑃, 𝑐1 , … , 𝑐n ∈ 𝜎A .
   Proposition 7 [14]. For the model 𝔄b and for an arbitrary sentence φ ∈ S(𝜎A ), we
have 𝔄b ⊨ φ ⇔ 𝑏 ≤ τ(φ).
          A Boolean-valued model 𝔄𝔹 = 〈𝐴, 𝜎A , 𝜏〉 is called atomic if the Boolean al-
gebra 𝔹 is atomic.
   Definition 8. Let 𝔄𝔹 be an atomic Boolean-valued model. Denote 𝐴𝑡(𝔹) =
{𝑎 ∈ 𝔹 | 𝑎 is an atom}. Consider the formal context (𝐴𝑡(𝔹), 𝑆(𝜎A ), 𝐼𝜏 ), where
                                  𝑎 𝐼𝜏 𝜑 ⇔ 𝑎 ≤ 𝜏(𝜑).

   Proposition 9. Let (𝐶, Γ) ∈ 𝔅(𝐴𝑡(𝔹), 𝑆(𝜎A ), 𝐼𝜏 ). Then Γ is a theory of the signa-
ture 𝜎A , i.e., for any 𝜑 ∈ S(𝜎A ) if Γ ⊢ 𝜑 then 𝜑 ∈ Γ.
   Proof. Let (𝐶, Γ) ∈ 𝔅(𝐴𝑡(𝔹), 𝑆(𝜎A ), 𝐼𝜏 ). Let us show that Γ is a theory. Suppose
that 𝜑 ∈ 𝑆(𝜎𝐴 ) and Γ ⊢ 𝜑. Prove that 𝜑 ∈ Γ. We have 𝐶 ′ = Γ; consequently, we must
only show that 𝜑 ∈ 𝐶′.




                           Fig. 2. The formal context (𝐴𝑡(𝔹), 𝑆(𝜎𝐴 ), 𝐼𝜏 ).
   Consider 𝑏 ∈ 𝐶, then 𝑏 ∈ 𝐴𝑡(𝔹). It is true that 𝐶 ′ = Γ, so for any 𝜓 ∈ Γ, we have
𝑏 𝐼𝜏 𝜓, therefore 𝑏 ≤ 𝜏(𝜓). Hence, by Proposition 7, we have 𝔄𝑏 ⊨ 𝜓.
   Consequently, for any 𝜓 ∈ Γ, it is true that 𝔄𝑏 ⊨ 𝜓, which means that 𝔄𝑏 ⊨ Γ. In-
volving the fact that Γ ⊢ 𝜑, we conclude that 𝔄𝑏 ⊨ 𝜑. Therefore, by Proposition 7,
we have 𝑏 ≤ 𝜏(𝜑), so 𝑏 𝐼𝜏 𝜑.
   Thus, we have proved that 𝑏 𝐼𝜏 𝜑 for any 𝑏 ∈ 𝐶. Then 𝜑 ∈ 𝐶 ′ = Γ. Therefore, we
have shown that for any 𝜑 ∈ 𝑆(𝜎𝐴 ), if Τ ⊢ 𝜑 then 𝜑 ∈ Τ. Hence, Γ is a theory.     ∎
    Theorem 10. Let 𝔄𝔹 = 〈𝐴, 𝜎A , 𝜏〉 be an atomic Boolean-valued model. There ex-
ists an atomic Boolean-valued model 𝔄𝔹1 = 〈𝐴, 𝜎A , 𝜏1 〉, where 𝜏1 : S(𝜎A ) → 𝔹1 , and
an epimorphism g: 𝔹→ 𝔹1 such that
    1) the formal context (𝐴𝑡(𝔹1 ), 𝑆(𝜎𝐴 ), 𝐼𝜏1 ) is object-clarified;
    2) for any φ ∈ S(𝜎A ) we have g(𝜏(𝜑)) = 𝜏1 (𝜑);
    3) for any 𝑏 ∈ At(𝔹), if 𝑔(𝑏) ≠ 0 then 𝑔(𝑏) ∈ At(𝔹1 );
    4) for any 𝑏 ∈ At(𝔹) and 𝜑 ∈ S(𝜎A ), if 𝑔(𝑏) ≠ 0 then 𝑏 𝐼𝜏 𝜑 ⇔ g(𝑏) 𝐼𝜏1 𝜑.
    Proof. Let 𝔄𝔹 = 〈𝐴, 𝜎A , 𝜏〉 be a Boolean-valued model and 𝔹 be atomic.




                             Fig. 3. Epimorphism 𝑔: 𝔹 → 𝔹1

   Suppose that the formal context (𝐴𝑡(𝔹), 𝑆(𝜎𝐴 ), 𝐼𝜏 ) is not object-clarified. Consider
an equivalence relation ~ on the set 𝐴𝑡(𝔹) of the atoms of the Boolean algebra 𝔹
defined as follows: for 𝑎, 𝑏 ∈ 𝐴𝑡(𝔹) we have 𝑎~𝑏 iff for any 𝜑 ∈ 𝑆(𝜎𝐴 ) it is true that
𝑎 𝐼𝜏 𝜑 ⇔ 𝑏 𝐼𝜏 𝜑.
   Consider the quotient set 𝔹/~ , and denote 𝐻 = 𝐴𝑡(𝔹)/~ .
   We chose exactly one element 𝑐[𝑎] ∈ [𝑎] in each equivalence class [𝑎] ∈ 𝐴𝑡(𝔹)/~ .
Denote
               𝐶 = {𝑐[𝑎] | [𝑎] ∈ 𝐻} ⊆ 𝐴𝑡(𝐵) and 𝑑 =              ⋃           𝑏.
                                                             (𝑏∈(𝐴𝑡(𝐵)\𝐶))
   Consider a principal ideal 𝐼 = 𝑑̂ = {𝑏 ∈ 𝔹 | 𝑏 ≤ 𝑑} of the Boolean algebra 𝔹 :
𝐼 ⊲ 𝔹.
   Consider a Boolean algebra 𝔹1 = 𝔹⁄𝐼 which is the quotient algebra of the Boolean
algebra 𝔹 by the ideal 𝐼.
   Consider an epimorphism 𝑔: 𝔹 → 𝔹1 defined as follows: 𝑔(𝑏) = 𝑏⁄𝐼 for any
𝑏 ∈ 𝔹; here 𝑏⁄𝐼 is the quotient class of the element 𝑏.
   Define a mapping 𝜏1 : 𝑆(𝜎𝐴 ) → 𝔹1 as follows:
                                   𝜏(𝜑)⁄
                        𝜏1 (𝜑) =        𝐼 for 𝜑 ∈ 𝑆(𝜎𝐴 ).
  Lemma 11. 𝔄𝔹1 = 〈𝐴, 𝜎𝐴 , 𝜏1 〉 is a Boolean-valued model.
  Proof. Consider 𝜑, 𝜓 ∈ 𝑆(𝜎𝐴 ). We have
                            𝜏(¬𝜑)⁄      𝜏(𝜑)⁄     𝜏(𝜑)⁄
                𝜏1 (¬𝜑) =           𝐼=        𝐼=       𝐼 = 𝜏1 (𝜑);

              𝜏(𝜑 ∨ 𝜓)⁄    𝜏(𝜑) ∪ 𝜏(𝜓)⁄    𝜏(𝜑)⁄     𝜏(𝜓)⁄
 𝜏1 (𝜑 ∨ 𝜓) =          𝐼=              𝐼=       𝐼 ∪       𝐼 = 𝜏1 (𝜑) ∪ 𝜏1 (𝜓);
              𝜏(𝜑&𝜓)⁄     𝜏(𝜑) ∩ 𝜏(𝜓)⁄    𝜏(𝜑)⁄     𝜏(𝜓)⁄
  𝜏1 (𝜑 &𝜓) =         𝐼=              𝐼=       𝐼 ∩       𝐼 = 𝜏1 (𝜑) ∩ 𝜏1 (𝜓);
                𝜏(𝜑 → 𝜓)⁄   𝜏(𝜑) ∪ 𝜏(𝜓)⁄   𝜏(𝜑)⁄   𝜏(𝜓)⁄
 𝜏1 (𝜑 → 𝜓) =            𝐼=             𝐼=      𝐼∪      𝐼 = 𝜏1 (𝜑) ∪ 𝜏1 (𝜓).

  Consider 𝜑(𝑥) ∈ 𝐹(𝜎𝐴 ). We have
                              𝜏(∀𝑥𝜑(𝑥))⁄   ⋂𝑎∈𝐴 𝜏(𝜑(𝑐𝑎 ))⁄
              𝜏1 (∀𝑥𝜑(𝑥)) =             𝐼=                𝐼=

                                   𝜏(𝜑(𝑐𝑎 ))⁄
                        =⋂                   𝐼 = ⋂ 𝜏1 (𝜑(𝑐𝑎 )) ;
                             𝑎∈𝐴                 𝑎∈𝐴


                                    𝜏(∃𝑥𝜑(𝑥))⁄   ⋃𝑎∈𝐴 𝜏(𝜑(𝑐𝑎 ))⁄
                 𝜏1 (∃𝑥𝜑(𝑥)) =                𝐼=                𝐼=

                                   𝜏(𝜑(𝑐𝑎 ))⁄
                         =⋃                  𝐼 = ⋃ 𝜏1 (𝜑(𝑐𝑎 )).
                             𝑎∈𝐴                 𝑎∈𝐴

  Note that the equalities

                         ⋂𝑎∈𝐴 𝜏(𝜑(𝑐𝑎 ))⁄    𝜏(𝜑(𝑐𝑎 ))⁄
                                        𝐼=⋂           𝐼
                                                𝑎∈𝐴

and

                         ⋃𝑎∈𝐴 𝜏(𝜑(𝑐𝑎 ))⁄    𝜏(𝜑(𝑐𝑎 ))⁄
                                        𝐼=⋃           𝐼
                                                𝑎∈𝐴

are true in virtue of the fact that the Boolean algebra 𝔹 is complete.
    Thus, we have shown that 𝔄𝔹1 = 〈𝐴, 𝜎A , 𝜏1 〉 is Boolean-valued model.
    The lemma is proved.                                                     ∎
   Continue the proof of the theorem. First we prove that the set of atoms
𝐴𝑡(𝔹1 ) = {𝑏⁄𝐼 | 𝑏 ∈ 𝐶}.
   Let 𝑏 ∈ 𝐶. Then 𝑏 ∉ 𝐼 and so, 𝑏⁄𝐼 ≠ 0. If 𝑐⁄𝐼 ≠ 0 and 𝑐⁄𝐼 ≤ 𝑏⁄𝐼 then

                              𝑐⁄ = 𝑐⁄ ∩ 𝑏⁄ = 𝑐 ∩ 𝑏⁄ .
                                𝐼    𝐼    𝐼        𝐼
   So, 𝑐 ∩ 𝑏 ≠ 0 and 𝑐 ∩ 𝑏 ≤ 𝑏, therefore, 𝑐 ∩ 𝑏 = 𝑏. Hence, 𝑐 ∩ 𝑏⁄𝐼 = 𝑏⁄𝐼 and so,
𝑐⁄ = 𝑏⁄ . Thus, 𝑏⁄ is an atom of the Boolean algebra 𝔹 .
  𝐼      𝐼          𝐼                                        1
   On the other hand, let 𝑐⁄𝐼 be an atom of the Boolean algebra 𝔹1 . Then 𝑐⁄𝐼 ≠ 0
and so, 𝑐 ≠ 0. The Boolean algebra 𝔹 is atomic, hence the set of atoms 𝐴𝑡(𝑐) =
{𝑏 ∈ 𝐴𝑡(𝔹)| 𝑏 ≤ 𝑐} ≠ ∅ and 𝑐 = ⋃𝑏∈𝐴𝑡(𝔹) 𝑏 . Involving the fact that 𝑐⁄𝐼 ≠ 0 we
conclude that 𝑐 ∉ 𝐼 = 𝑑̂, consequently, 𝑐 ≰ 𝑑.
   We have 𝑑 = ⋃𝑏∈𝐴𝑡(𝔹)\𝐶 𝑏 and 𝑐 = ⋃𝑏∈𝐴𝑡(𝑐) 𝑏, hence, if 𝐴𝑡(𝑐) ⊆ 𝐴𝑡(𝔹)\𝐶 then
𝑐 ≤ 𝑑. Therefore, 𝐴𝑡(𝑐) ⊈ 𝐴𝑡(𝔹)\𝐶, so 𝐴𝑡(𝑐) ∩ 𝐶 ≠ ∅.
   Consequently, there exists an atom 𝑏 ∈ 𝐴𝑡(𝑐) ∩ 𝐶 . Hence, 𝑏 ∈ 𝐶 and 𝑏 ≤ 𝑐 , so
𝑏⁄ ≤ 𝑐⁄ . As we proved above, 𝑏 ∈ 𝐶 implies that 𝑏⁄ is an atom of the Boolean
  𝐼      𝐼                                                  𝐼
algebra 𝔹1 . Involving the fact that 𝑐⁄𝐼 is an atom we conclude that 𝑏⁄𝐼 = 𝑐⁄𝐼 and so,
𝑐⁄ ∈ {𝑒⁄ | 𝑒 ∈ 𝐶}. Therefore, 𝐴𝑡(𝔹 ) = {𝑏⁄ | 𝑏 ∈ 𝐶}.
  𝐼       𝐼                              1         𝐼
   Thus, that for any 𝑏 ∈ 𝐴𝑡(𝔹) if 𝑏 ∈ 𝐴𝑡(𝔹)\𝐶 then 𝑏 ≤ 𝑑, hence, 𝑏⁄𝐼 = 0. If
𝑏 ∈ 𝐶 then 𝑏⁄𝐼 ∈ 𝐴𝑡(𝔹1 ). Consequently, the statement (3) holds.
   Next, by the definition of the epimorphism 𝑔: 𝔹 → 𝔹1 we have
                                           𝜏(𝜑)⁄
                              𝑔(𝜏(𝜑)) =           𝐼 = 𝜏1 (𝜑).
   Therefore, the statement (2) holds.
   Lemma 12. For every 𝑏 ∈ 𝐴𝑡(𝔹), and every 𝜑 ∈ 𝑆(𝜎𝐴 ), if 𝑔(𝑏) ≠ 0 then
                               𝑏 𝐼𝜏 𝜑 ⇔ 𝑔(𝑏) 𝐼𝜏1 𝜑.
   Proof. Consider 𝑏 ∈ 𝐴𝑡(𝔹) and 𝜑 ∈ 𝑆(𝜎𝐴 ) . Let 𝑔(𝑏) ≠ 0 . Let us prove that
𝑏 𝐼𝜏 𝜑 ⇔ 𝑔(𝑏) 𝐼𝜏1 𝜑.
                                                                 𝜏(𝜑)⁄
   (⇒) Suppose that 𝑏 𝐼𝜏 𝜑 holds. Then 𝑏 ≤ 𝜏(𝜑) , hence 𝑏⁄𝐼 ≤          𝐼 = 𝜏1 (𝜑) .
                    𝑏
Therefore, we have ( ⁄𝐼 ) 𝐼𝜏1 𝜑 and so, 𝑔(𝑏)𝐼𝜏1 𝜑 holds.
    (⇐) Suppose that 𝑏 𝐼𝜏 𝜑 doesn’t hold. Then 𝑏 ≰ 𝜏(𝜑), so, 𝑏 ≠ 𝑏 ∩ 𝜏(𝜑). The el-
ement 𝑏 is an atom and we have 𝑏 ≠ 𝑏 ∩ 𝜏(𝜑) ≤ 𝑏. Then 𝑏 ∩ 𝜏(𝜑) = 0, hence
𝑏⁄ ∩ 𝜏(𝜑)⁄ = 𝑏 ∩ 𝜏(𝜑)⁄ = 0.
   𝐼          𝐼            𝐼
                                                    𝜏(𝜑)⁄                  𝜏(𝜑)⁄
    Since ⁄𝐼 = 𝑔(𝑏) ≠ 0 , we have 𝑏⁄𝐼 ≠ 𝑏⁄𝐼 ∩
           𝑏                                                          𝑏
                                                           𝐼 , hence, ⁄𝐼 ≰      𝐼=
𝜏1 (𝜑), i.e., 𝑔(𝑏) ≰ 𝜏1 (𝜑). Therefore, 𝑔(𝑏)𝐼𝜏1 𝜑 doesn’t hold.
    The lemma is proved.                                                         ∎
   Thus, we have proved the statement (4). Now let us prove that the formal context
(𝐴𝑡(𝔹1 ), 𝑆(𝜎𝐴 ), 𝐼𝜏1 ) is object-clarified – the statement (1).
                                 𝑏        𝑏
   Consider 𝑏1 , 𝑏2 ∈ 𝐶. Let 1⁄𝐼 ≠ 2⁄𝐼 . Then there are atoms 𝑎1 , 𝑎2 ∈ 𝐴𝑡(𝔹) such
that 𝑏1 = 𝑐[𝑎1] and 𝑏2 = 𝑐[𝑎2] . Hence, 𝑏1 ∈ [𝑎1 ] and 𝑏2 ∈ [𝑎2 ]. Since 𝑏1 ≠ 𝑏2 , we
have [𝑎1 ] ≠ [𝑎2 ], so, 𝑏1 ≁ 𝑏2 . Therefore, there is a sentence 𝜑 ∈ 𝑆(𝜎𝐴 ) such that only
one of the statements 𝑏1 𝐼𝜏 𝜑 and 𝑏2 𝐼𝜏 𝜑 holds. Suppose that 𝑏1 𝐼𝜏 𝜑 holds and 𝑏2 𝐼𝜏 𝜑
doesn’t hold. We conclude by Lemma 12 that 𝑔(𝑏1 ) 𝐼𝜏1 𝜑 holds and 𝑔(𝑏2 ) 𝐼𝜏1 𝜑
                                                                   𝑏          𝑏
doesn’t hold. Therefore, the rows corresponding to the objects 1⁄𝐼 and 2⁄𝐼 of the
formal context (𝐴𝑡(𝔹1 ), 𝑆(𝜎𝐴 ), 𝐼𝜏1 ) are different. Thus, the formal context
(𝐴𝑡(𝔹1 ), 𝑆(𝜎𝐴 ), 𝐼𝜏1 ) is object-clarified.
   The theorem is proved.                                                   ∎
   Recall that 𝕂(𝜎A ) = {〈{𝑐𝑎𝔄 | 𝑎 ∈ 𝐴}, 𝜎A 〉 | 𝑐𝑎𝔄 ≠ 𝑐𝑏𝔄 for 𝑎 ≠ 𝑏} and
𝑇ℎ(𝐾) = {𝜑 ∈ S(𝜎A )| 𝐾 ⊨ 𝜑} is the theory of the class 𝐾 ⊆ 𝕂(𝜎A ).
   We represent the set of the cases of the domain (3rd level of the ontological model)
as a class of models 𝐾 ⊆ 𝕂(𝜎A ). So, it is interesting and important to solve the fol-
lowing
   Problem 13. How to describe the theories of the classes 𝐾 ⊆ 𝕂(𝜎A ).
   Theorem 14. Let 𝑇 be a theory of the signature 𝜎𝐴 . There exists a class 𝐾 ⊆ 𝕂(𝜎𝐴 )
such that 𝑇 = 𝑇ℎ(𝐾) if and only if there exists a Bolean-valued model 𝔄𝔹 such that
                             (𝑇 ′ , 𝑇) ∈ 𝔅(𝐴𝑡(𝔹), 𝑆(𝜎𝐴 ), 𝐼𝜏 ).
   Proof. Let 𝑇 be a theory in the signature 𝜎𝐴 .
   (⇒) Consider a class 𝐾 ⊆ 𝕂(𝜎𝐴 ). Let 𝑇 = 𝑇ℎ(𝐾). Denote 𝐾0 = 𝕂(𝜎𝐴 ). Consider
a Boolean algebra 𝔹 = 〈℘(𝐾0 ); ∪,∩, −, ∅, 𝐾0 〉 and a mapping 𝜏: 𝑆(𝜎𝐴 ) → 𝔹 defined
as follows: 𝜏(𝜑) = {𝔅 ∈ 𝐾 | 𝔅 ⊨ 𝜑} for a sentence 𝜑 ∈ 𝑆(𝜎𝐴 ).
   Lemma 15. 𝔄𝔹 = 〈𝐴, 𝜎𝑎 , 𝜏〉 is a Boolean-valued model.
   Proof. Let 𝜑, 𝜓 ∈ 𝑆(𝜎𝐴 ). Then
                𝜏(¬𝜑) = {𝔅 ∈ 𝐾0 | 𝔅 ⊨ ¬𝜑} = {𝔅 ∈ 𝐾0 | 𝔅 ⊭ 𝜑} =
                      𝐾\{𝔅 ∈ 𝐾0 | 𝔅 ⊨ 𝜑} = 𝐾0 \𝜏(𝜑) = 𝜏(𝜑);
                       𝜏(𝜑 ∨ 𝜓) = {𝔅 ∈ 𝐾0 | 𝔅 ⊨ (𝜑 ∨ 𝜓)} =
             = {𝔅 ∈ 𝐾0 | 𝔅 ⊨ 𝜑} ∪ {𝔅 ∈ 𝐾0 | 𝔅 ⊨ 𝜓} = 𝜏(𝜑) ∪ 𝜏(𝜓);
                     𝜏(𝜑&𝜓) = {𝔅 ∈ 𝐾0 | 𝔅 ⊨ (𝜑&𝜓)} =
            = {𝔅 ∈ 𝐾0 | 𝔅 ⊨ 𝜑} ∩ {𝔅 ∈ 𝐾0 | 𝔅 ⊨ 𝜓} = 𝜏(𝜑) ∩ 𝜏(𝜓);
             𝜏(𝜑 → 𝜓) = {𝔅 ∈ 𝐾0 | 𝔅 ⊨ (𝜑 ∨ 𝜓)} = 𝜏(𝜑) ∪ 𝜏(𝜓).
  Let 𝜑(𝑥) ∈ 𝐹(𝜎𝐴 ). Then
                     𝜏(∀𝑥𝜑(𝑥)) = {𝔅 ∈ 𝐾0 | 𝔅 ⊨ ∀𝑥𝜑(𝑥)} =
 = {𝔅 ∈ 𝐾0 | 𝔅 ⊨ 𝜑(𝑎) for any 𝑎 ∈ 𝐴} = {𝔅 ∈ 𝐾0 | 𝔅 ⊨ 𝜑(𝑐𝑎 ) for any 𝑎 ∈ 𝐴} =
                    = ⋂{𝔅 ∈ 𝐾0 | 𝔅 ⊨ 𝜑(𝑐𝑎 )} = ⋂ 𝜏(𝜑(𝑐𝑎 )) ;
                      𝑎∈𝐴                           𝑎∈𝐴
                   𝜏(∃𝑥𝜑(𝑥)) = {𝔅 ∈ 𝐾0 | 𝔅 ⊨ ∃𝑥𝜑(𝑥)} =
 {𝔅 ∈ 𝐾0 | 𝔅 ⊨ 𝜑(𝑎) for some 𝑎 ∈ 𝐴} = {𝔅 ∈ 𝐾0 | 𝔅 ⊨ 𝜑(𝑐𝑎 ) for some 𝑎 ∈ 𝐴} =
                   = ⋃{𝔅 ∈ 𝐾0 | 𝔅 ⊨ 𝜑(𝑐𝑎 )} = ⋃ 𝜏(𝜑(𝑐𝑎 )).
                      𝑎∈𝐴                          𝑎∈𝐴
  The lemma is proved.                                                              ∎

   Notice that the atoms of the Boolean algebra 𝔹 = 〈℘(𝐾0 ); ∪,∩, −, ∅, 𝐾0 〉 are exact-
ly the one-element subsets of the set 𝐾0 . Hence, 𝐴𝑡(𝔹) = {{𝔅} | 𝔅 ∈ 𝐾0 }.
  Consider a formal context 〈𝐴𝑡(𝔹), 𝑆(𝜎𝐴 ), 𝐼𝜏 〉. Let ℭ ∈ 𝐾0 and 𝜑 ∈ 𝑆(𝜎𝐴 ). Then we
have
         {ℭ} 𝐼𝜏 𝜑 ⇔ {ℭ} ⊆ 𝜏(𝜑) ⇔ {ℭ} ⊆ {𝔅 ∈ 𝐾 | 𝔅 ⊨ 𝜑} ⇔ ℭ ⊨ 𝜑.
    Thus, we have {ℭ} 𝐼𝜏 𝜑 ⇔ ℭ ⊨ 𝜑. Recall that 𝐾 ⊆ 𝐾0 = 𝕂(𝜎𝐴 ) and 𝑇 = 𝑇ℎ(𝐾).
    Denote 𝐾̃ = {{𝔅} | 𝔅 ∈ 𝐾} ⊆ 𝐴𝑡(𝔹). Then
       ̃ ′ = {𝜑 ∈ 𝑆(𝜎𝐴 ) | {𝔅} 𝐼𝜏 𝜑 for any {𝔅} ∈ 𝐾
       𝐾                                          ̃}
                            = {𝜑 ∈ 𝑆(𝜎𝐴 ) | 𝔅 ⊨ 𝜑 for any 𝔅 ∈ 𝐾} = 𝑇ℎ(𝐾) = 𝑇.
  Therefore, 𝑇 = 𝑇 and the pair (𝑇 ′ , 𝑇) is a formal concept of the formal context
                     ′′

〈𝐴𝑡(𝔹), 𝑆(𝜎𝐴 ), 𝐼𝜏 〉, i.e., (𝑇 ′ , 𝑇) ∈ 𝔅(𝐴𝑡(𝔹), 𝑆(𝜎𝐴 ), 𝐼𝜏 ).
  (⇐) Let 𝔄𝔹 = 〈𝐴, 𝜎𝑎 , 𝜏〉 be a Boolean-valued model and a pair (𝑇 ′ , 𝑇) ∈
𝔅(𝐴𝑡(𝔹), 𝑆(𝜎𝐴 ), 𝐼𝜏 ).`
    Denote 𝐶 = 𝑇 ′ . Then 𝐶 ⊆ 𝐴𝑡(𝔹) and 𝐶 ′ = 𝑇. Consider a class 𝐾 = {𝔄𝑏 | 𝑏 ∈ 𝐶}.
We have proved above in the proof of Proposition 9 that in this case 𝔄𝑏 ⊨ 𝑇 holds for
any 𝑏 ∈ 𝐶.
    Therefore, for any 𝔅 ∈ 𝐾 we have 𝔅 ⊨ 𝑇 . It means that 𝐾 ⊨ 𝑇 . Hence, 𝑇 ⊆
𝑇ℎ(𝐾) = {𝜑 ∈ 𝑆(𝜎𝐴 )| 𝐾 ⊨ 𝜑}.
    Let us show that 𝑇ℎ(𝐾) ⊆ 𝑇. Let 𝜑 ∈ 𝑇ℎ(𝐾). Then 𝐾 ⊨ 𝜑, which means that
𝔅 ⊨ 𝜑 for any 𝔅 ∈ 𝐾. Consequently, for any 𝑏 ∈ 𝐶 we have 𝔄𝑏 ⊨ 𝜑. By Proposition
7, 𝔄𝑏 ⊨ 𝜑 implies that 𝑏 ≤ 𝜏(𝜑), hence, 𝑏 𝐼𝜏 𝜑 holds.
    Thus, for any 𝑏 ∈ 𝐶 we have 𝑏 𝐼𝜏 𝜑, then 𝜑 ∈ 𝐶 ′ = 𝑇 ′′ = 𝑇, i.e., 𝜑 ∈ 𝑇. Therefore,
for any 𝜑 ∈ 𝑇ℎ(𝐾) we have 𝜑 ∈ 𝑇, hence 𝑇ℎ(𝐾) ⊆ 𝑇, and so, 𝑇 = 𝑇ℎ(𝐾).
    The theorem is proved.                                                           ∎


5       Conclusion

In the present paper we investigate the mathematical foundations of ontological mod-
eling of the domain of mobile networks. We use the four-level model of knowledge
representation to formalize this domain. We construct the case model at the third level
of ontological model creation, when we formalize the empirical knowledge. The case
model is presented by a set of countable algebraic systems. In the ontological model,
the high-level characteristics of mobile network subscribers are represented with the
help of first order theories of classes of algebraic systems of the special kind.
   Next, we describe a method of constructing a formal context for a Boolean-valued
model which represents the case model. We show that, without loss of generality, we
may consider only object-clarified formal contexts corresponding to the Boolean-
valued models.
   We prove that the intents of formal concepts of formal contexts corresponding to
Boolean-valued models are first order theories of the signature under consideration. In
the end, we solve the following problem: What are the theories of the classes
𝐾 ⊆ 𝕂(𝜎A )? We obtain a description of theories of the classes of domain cases in the
language of formal concepts of the formal contexts corresponding to the Boolean-
valued models.


       References
 1. Naydanov, Ch., Palchunov, D., Sazonova, P.: Development of automated methods for the
    prevention of risks of critical conditions, based on the analysis of the knowledge extracted
    from the medical histories. Proceedings of the International Conference on Biomedical
    Engineering and Computational Technologies, Novosibirsk, 47-52 (2015)
 2. Palchunov, D., Yakhyaeva, G., Yasinskaya, O.: Software system for diagnosing spinal dis-
    eases using case-based reasoning. Proceedings - 2015 International Conference on Bio-
    medical Engineering and Computational Technologies, SIBIRCON 2015, 205-210 (2015)
 3. Chang, C.C., Keisler, H.J.: Model theory: 3rd ed. Amsterdam, New York: North-Holland,
    Elsevier Science Pub. Co. (1990)
 4. Pal'chunov, D., Yakhyaeva, G.: Fuzzy logics and fuzzy model theory. Algebra and Logic,
    54 (1), 74-80 (2015)
 5. Kuznetsov, S.O., Poelmans, J.: Knowledge representation and processing with formal con-
    cept analysis. Wiley Interdisciplinary Reviews: Data Mining and Knowledge Discovery 3
    (3), 200-215 (2013)
 6. Poelmans, J., Kuznetsov, S.O., Ignatov, D.I., Dedene, G.: Formal concept analysis in
    knowledge processing: A survey on models and techniques. Source of the Document Ex-
    pert Systems with Applications, 40 (16), 6601-6623 (2013)
 7. Pal’chunov, D.: Lattices of relatively axiomatizable classes. Lecture Notes in Artificial In-
    telligence, 4390, 221–239 (2007)
 8. Palchunov, D., Yakhyaeva, G., Dolgusheva E.: Conceptual Methods for Identifying Needs
    of Mobile Network Subscribers. International Conference on Concept Lattices and Their
    Applications CLA 2016, 147-158 (2016)
 9. Palchunov, D.: The solution of the problem of information retrieval based on ontologies.
    Bisnes-informatika, 1, 3–13 (2008) (In Russ.)
10. Palchunov, D.: Virtual catalog: the ontology-based technology for information retrieval.
    In: Knowledge Processing and Data Analysis. LNAI 6581, Springer-Verlag Berlin Heidel-
    berg, 164–183 (2011)
11. Pulchunov, D., Yakhyaeva G.: Interval fuzzy algebraic systems. Mathematical Logic in
    Asia. Proceedings of the 9-th Asian Logic Conference. World Scientific Publishers. 191-
    202 (2006)
12. Yakhyaeva, G., Yasinkaya, O.: An algorithm to compare computer-security knowledge
    from different sources. ICEIS 2015 - 17th International Conference on Enterprise Infor-
    mation Systems, Proceedings 1, 565-572 (2015)
13. Yakhyaeva, G.: Logic of fuzzifications. Proceedings of the 4th Indian International Con-
    ference on Artificial Intelligence, IICAI 2009, 222-239 (2009)
14. Pal’chunov, D., Yakhyaeva, G.: Fuzzy algebraic systems. Vestnik NGU, Mat., Mekh., Inf.,
    10, No. 3, 76-93 (2010)

</pre>