=Paper= {{Paper |id=Vol-3184/MK_short2 |storemode=property |title=Multi Context Model Counting |pdfUrl=https://ceur-ws.org/Vol-3184/MK_short2.pdf |volume=Vol-3184 |authors=Luciano Serafini |dblpUrl=https://dblp.org/rec/conf/esws/Serafini22 }} ==Multi Context Model Counting== https://ceur-ws.org/Vol-3184/MK_short2.pdf 
Multi Context Model Counting
Luciano Serafini
Fondazione Bruno Kessler, Trento, Italy


                                      Abstract
                                      Contextual reasoning is the result of the composition of local reasoning in each context via a set of
                                      inference rules, called bridge rules. In the past it has been argued that organizing knowledge in multi-
                                      ple related contexts (modules) provides many advantages. Logical inference and satisfiability in multi
                                      context systems have been widely studied. However,there are other important inference tasks such as
                                      model counting and weighted model counting that one want to perform on an MCS. In this note we
                                      concentrate on Model Counting task that can provide a good base for probabilistic reasoning in Multi
                                      Context Systems. The paper proposes a method that computes model counting for a multi context
                                      system in terms of the combination of model counting in each context.




1. Introduction
Multi Context Systems (MCSs) [1, 2, 3, 4, 5, 6] are logical frameworks that allow modelling
knowledge distributed amongst a set theories called contexts. Each theory is specified in a
(possibly different) logical language, called local language. The fact that a formula πœ‘ holds in
a context 𝑐 is expressed by the labelled formula 𝑐 : πœ‘. The connections between knowledge
of different contexts are modeled by the so called bridge rules, which are inference rules with
premises and conclusions in different contexts. An interpretation of an MCS maps every
context in a set of interpretations of the local language, called local interpretations. An MCS
interpretation is a model if local interpretations satisfy local theories and the combination of
local interpretations satisfy the bridge rules. Model counting for MCS is the task of determining
the cardinality of the set of models of an MCS.
   Model counting for logical system is obtaining increasing attentions due to its important role
in the modern approaches of AI [7], where logical reasoning are blended with some form of
quantitative inference such as for instance probability. The aim of this paper is to investigate
about model counting method for MCS that exploit the intrinsic modular structure available
in an MCS. To the best of our knowledge this is the first attempt to solve the model counting
problem for MCSs. The paper provides theoretical result that proves how model counting in
MCS can be obtained by a suitable combination of algorithms for model counting in each single
context.




Modular Knowledge 2022 - 1st Workshop on Modular Knowledge ESWC 2022, Hersonissos, Greece, May 29, 2022
" serafini@fbk.eu (L. Serafini)
                                    Β© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
 CEUR
 Workshop
 Proceedings
               http://ceur-ws.org
               ISSN 1613-0073
                                    CEUR Workshop Proceedings (CEUR-WS.org)
2. Multi context systems
Let 𝐢 be a set. Every element of 𝐢 is called context. A Multi  Context System      on a family of
logical languages 𝐿 = {𝐿𝑐 }π‘βˆˆπΆ , is a structure MC = {Φ𝑐 }π‘βˆˆπΆ , BR where Φ𝑐 is a set of
                                                         βŸ¨οΈ€                βŸ©οΈ€

closed formulas of the language 𝐿𝑐 and BR is a set of bridge rules, i.e., expressions of the form

                             𝑐1 : πœ‘1 , . . . , 𝑐𝑛 : πœ‘π‘› β‡’ 𝑐𝑛+1 : πœ‘π‘›+1                   (1)

where πœ‘π‘– is a sentential formula of 𝐿𝑐𝑖 . A model for an MCS {Φ𝑐 }π‘βˆˆπΆ , BR is a structure
                                                                   βŸ¨οΈ€     βŸ©οΈ€

Ξ© = {Ω𝑐 }π‘βˆˆπΆ where
       1. Ω𝑐 is a set of interpretations of 𝐿𝑐 such that for all πœ” ∈ Ω𝑐 , πœ” |= Φ𝑐 (written as Ω𝑐 |= Φ𝑐 );
       2. For every bridge rule of the form (1) in BR, if Ω𝑐𝑖 |= πœ‘π‘– for all 𝑖 = 1, . . . , 𝑛, then
          Ω𝑐𝑛+1 |= πœ‘π‘›+1
By considering each πœ‘ ∈ Φ𝑐 as a rule with zero premises, an MCS can be seen as a set of bridge
rules BR. In the following we consider this simpler form of an MCS.

Example 1. Alice and Bob are two agents who have beliefs about two propositions 𝑝 and π‘ž. Bob
can query Alice on her beliefs about 𝑝 and π‘ž, Alice can have partial or contraddictory beliefs
about 𝑝 and π‘ž, therefore, it is possible that Alice provides no answer or contraddictory answers
to Bob’s queries. Bob has the following beliefs about Alice. He believes that, if Alice is reliable
(π‘Ÿ), then Alice’s answers are correct, and therefore he will also believe in what Alice says. This
simple scenario can be formulated with an MCS 𝑀 πΆπ‘Žπ‘ with two contexts 𝐢 = {π‘Ž, 𝑏}; where the
local languages πΏπ‘Ž and 𝐿𝑏 are s propositional languages on the propositions {𝑝, π‘ž} and {𝑝, π‘ž, π‘Ÿ}
respectively, The two contexts are connected by the following bridge rules:

                         π‘Ž:𝑝⇒𝑏:π‘Ÿβ†’π‘                                  π‘Ž : ¬𝑝 β‡’ 𝑏 : π‘Ÿ β†’ ¬𝑝                           (2)
                         π‘Ž:π‘žβ‡’π‘:π‘Ÿβ†’π‘ž                                  π‘Ž : Β¬π‘ž β‡’ 𝑏 : π‘Ÿ β†’ Β¬π‘ž                           (3)

The above bridge rules simulate all the query-answering interactions between Alice and Bob. No-
tice that if Alice provides contraddictory answers, e.g., π‘Ž : 𝑝 and π‘Ž : ¬𝑝 then Bob will believe that
she is not reliable (𝑏 : Β¬π‘Ÿ. A model for 𝑀 πΆπ‘Žπ‘ is a pair βŸ¨β„¦π‘Ž , Ω𝑏 ⟩, where β„¦π‘Ž and Ω𝑏 represent the
final belief state of the two agents after Bob have done all the possible queries to Alice. We are
interested in counting the number of final states of such a simple system, i.e., the number of models
of 𝑀 πΆπ‘Žπ‘ .


3. Multi context model counting
Suppose that for every language context 𝑐, there is an oracle mc 𝑐 that returns the number of
models mc 𝑐 (Ξ¦)1 for every set of 𝐿𝑐 -sentences Ξ¦. We are interested in finding a way to solve
the model counting problem for BR using such oracles.
  Let 𝐡 be the set of labelled formulas 𝑐 : πœ‘ contained in in some bridge rule of BR. Let 𝐹 βŠ† 𝐡
be any subset of 𝐡 closed under BR. Let F be the set of all such 𝐹 ’s. Let’s define mc(𝐹 ) as the
number of Ξ© = {Ω𝑐 }π‘βˆˆπΆ , where Ω𝑐 is a set of models for 𝐿𝑐 , such that:
1
    When it is clear from the context we will omit the index to the context and use the simpler notation mc(πœ‘).
   1. Ω𝑐 |= πœ‘ for every 𝑐 : πœ‘ ∈ 𝐹 and
   2. Ω𝑐 ΜΈ|= πœ‘ for every 𝑐 : πœ‘ ∈ 𝐹
                                 Β― = 𝐡 βˆ– 𝐹.

Notice that Ξ© satisfies conditions 1 and 2 if and only if Ξ© is a model of BR.

Proposition 1. Ξ© cannot satisfy conditions 1 and 2 for two distinct 𝐹 and 𝐹 β€² .

Proof: If 𝐹 ΜΈ= 𝐹 β€² there is a labelled formula 𝑐 : πœ‘ such that either 𝑐 : πœ‘ ∈ 𝐹 ∩ 𝐹       Β― β€² or
𝑐:πœ‘βˆˆπΉ    Β― ∩ 𝐹 β€² . If Ξ© satisfies condition 1 and 2 for both 𝐹 and 𝐹 β€² then Ω𝑐 |= πœ‘ and Ω𝑐 ΜΈ|= πœ‘,
which is a contradiction.                                                                      β–‘

Lemma 1. For every 𝐹 βŠ† 𝐡:
                                          ∏︁ βˆ‘οΈ
                              π‘šπ‘(𝐹 ) =                (βˆ’1)|𝐺| 2π‘šπ‘(𝐹𝑐 βˆͺ𝐺)
                                               ¯𝑐
                                           𝑐 πΊβŠ†πΉ


where, for every set of labelled formulas 𝑋, 𝑋𝑐 denotes the set {πœ‘ | 𝑐 : πœ‘ ∈ 𝑋}.

  Proof: For a given 𝐹 , an MC interpretation Ξ© = {Ω𝑐 }π‘βˆˆπΆ satisfies all the 𝑐 : πœ‘ in 𝐹 and does
not satisfy all the 𝑐 : πœ‘ ∈ 𝐹
                            Β― if and only if it satisfies the following two conditions for every
𝑐 ∈ 𝐢:
   1. for all πœ‘ ∈ 𝐹𝑐 , πœ” |= πœ‘ for all πœ” ∈ Ω𝑐 ;
   2. for all πœ‘ ∈ 𝐹
                  Β― 𝑐 , πœ” |= Β¬πœ‘ for some πœ” ∈ Ω𝑐 .

Therefore we have to count how many such a Ω𝑐 exist for every 𝑐. For this purpose we use the
following result:

Corollary 1 ([8] section 4.2). Let 𝑋 be a set of objects and let 𝒴 = {π‘Œ1 , . . . , π‘Œπ‘š } be a set of
subsets of 𝑋. For every 𝒬 βŠ† 𝒴, βƒ’let 𝑁 (βŠ‡ 𝒬) βƒ’be the count of objects in 𝑋 that belong to all the
                                   βƒ’ β‹‚οΈ€                                          βˆ‘οΈ€
subsets π‘Œπ‘– ∈ 𝒬, i.e., 𝑁 (βŠ‡ 𝒬) = βƒ’{ π‘Œπ‘– βˆˆπ‘„ π‘Œπ‘– }βƒ’. For every 0 ≀ 𝑙 ≀ π‘š, let 𝑠𝑙 = |𝒬|=𝑙 𝑁 (βŠ‡ 𝒬)
                                                βƒ’
and let 𝑒0 be count of objects that do not belong to any of the π‘Œπ‘– in 𝒴, then
                                                 π‘š
                                                βˆ‘οΈ
                                         𝑒0 =         (βˆ’1)𝑙 𝑠𝑙                                    (4)
                                                𝑙=0

In our case, let 𝑋 be the set of all the subsets of models of 𝐹𝑐 . I.e. 𝑋 = {Ω βŠ† Ω(𝐿𝑐 ) | Ω |= 𝐹𝑐 },
where Ω(𝐿𝑐 ) is the set of all interpretations of 𝐿𝑐 . Let 𝒴 = {π‘Œπœ‘ }πœ‘βˆˆπΉΒ― 𝑐 , where π‘Œπœ‘ = {Ω ∈ 𝑋 |
Ω |= πœ‘}. With this definition we have that π‘’π‘œ is the number of subsets of 𝑋 (models of 𝐹𝑐 ) that
do not satisfy none of the formulas in 𝐹  Β― 𝑐 . To apply Corollary 1 we need to calculate 𝑠𝑙 for every
0 ≀ 𝑙 ≀ |𝐹¯ 𝑐 |. By definition of 𝑠𝑙 we have:
                                                               βƒ’        βƒ’
                                                               βƒ’        βƒ’
                                       βˆ‘οΈ                 βˆ‘οΈ βƒ’ ⋂︁ βƒ’
                                𝑠𝑙 =        𝑁 (βŠ‡ 𝒬) =          βƒ’
                                                               βƒ’    π‘Œπœ‘ βƒ’βƒ’
                                      |𝒬|=𝑙              πΊβŠ†πΉΒ― 𝑐 πœ‘βˆˆπΊ
                                                               βƒ’        βƒ’
                                                          |𝐺|=𝑙
                                                                     βƒ’β‹‚οΈ€      βƒ’
Notice that Ω ∈ πœ‘βˆˆπΊ π‘Œπœ‘ if and only if Ω |= 𝐹𝑐 ∧ 𝐺. This implies that βƒ’ πœ‘βˆˆπΊ π‘Œπœ‘ βƒ’ is the number
                 β‹‚οΈ€                                                  βƒ’        βƒ’
of subsets of the set of models that satisfiey 𝐹𝑐 ∧ 𝐺, i.e.,
                                             βˆ‘οΈ
                                      𝑠𝑙 =        2π‘šπ‘(𝐹𝑐 ∧𝐺)
                                            πΊβŠ†πΉΒ―π‘
                                            |𝐺|=𝑙


From which we conclude that the number of sets of models that satisfies 𝐹𝑐 and do not satisfy
Β― 𝑐 is:
𝐹
                                   βˆ‘οΈ
                              𝑒0 =      (βˆ’1)|𝐺| 2π‘šπ‘(𝐹𝑐 βˆͺ𝐺)
                                         ¯𝑐
                                       πΊβŠ†πΉ

Notice that every model of 𝐹 that does not satisfy the formulas in 𝐹¯ can be obtained by
selecting  for every 𝑐 a set of models that satisfy 𝐹𝑐 and do not satisfy 𝐹
                                                                          Β― 𝑐 . Since we have
              |𝐺| π‘šπ‘(𝐹   βˆͺ𝐺) of such sets of models, we can conclude that
βˆ‘οΈ€
      Β― 𝑐 (βˆ’1) 2
                       𝑐
   πΊβŠ†πΉ
                                        ∏︁ βˆ‘οΈ
                             π‘šπ‘(𝐹 ) =               (βˆ’1)|𝐺| 2π‘šπ‘(𝐹𝑐 βˆͺ𝐺)                        (5)
                                             ¯𝑐
                                         𝑐 πΊβŠ†πΉ

                                                                                              (6)

                                                                                               β–‘

Theorem 1.
                                       βˆ‘οΈ       ∏︁ βˆ‘οΈ
                       mc(BR) =                          (βˆ’1)|𝐺| 2π‘šπ‘(𝐹𝑐 βˆͺ𝐺)                   (7)
                                                  ¯𝑐
                                     𝐹 ∈F(BR) 𝑐 πΊβŠ†πΉ


  Proof: For every model Ξ© of BR there is an 𝐹 such that Ω |= 𝐹 and for every 𝑐 : πœ‘ ∈ 𝐹    Β―
Ω𝑐 ΜΈ|= πœ‘. Furthermore, Proposition 1 guarantees that Ξ© cannot be a model of two distinct 𝐹 ’s.
This allows us to infer that
                                      βˆ‘οΈ
                        mc(BR) =           mc(𝐹 )
                                     𝐹 ∈F(BR)
                                       βˆ‘οΈ       ∏︁ βˆ‘οΈ
                                 =                       (βˆ’1)|𝐺| 2π‘šπ‘(𝐹𝑐 βˆͺ𝐺)
                                                  ¯𝑐
                                     𝐹 ∈F(BR) 𝑐 πΊβŠ†πΉ

                                                                                              β–‘
   Notice that the set F(BR) can be computed by starting from any subset of 𝐡 and by applying
bridge rules until a fixpoint is reached. This operation takes at most |BR| steps. In the worse
case at every step only one element of BR is fired. Furthermore one can compute and cash
π‘šπ‘(𝑋𝑐 ) for all the subset 𝑋𝑐 βŠ† 𝐡𝑐 . The complexity of this is fully determined by mc 𝑐 and it is
not influenced by the complexity of the model counting in the other contexts. Therefore the
complexity of the entire process is just the sum of the complexity of computing model count in
𝑐 for all the subsets of 𝐡𝑐 .
Example 2 (continuation of Example 1). Let us apply Theorem ?? to a simplified version of
Example 1, where πΏπ‘Ž contains the only proposition 𝑝 and 𝐿𝑏 π‘Ÿ and 𝑝 we consider only bridge rules
(2). The set 𝐡 is equal to:

                             𝐡 = {π‘Ž : 𝑝, π‘Ž : ¬𝑝, 𝑏 : π‘Ÿ β†’ 𝑝, 𝑏 : π‘Ÿ β†’ ¬𝑝}

The set F of subsets 𝐹 of 𝐡 closed under the bridge rules (2) and (3), are the following:

                             𝐹0 = {}
                             𝐹1 = {𝑏 : π‘Ÿ β†’ 𝑝}
                             𝐹2 = {𝑏 : π‘Ÿ β†’ ¬𝑝}
                             𝐹3 = {𝑏 : π‘Ÿ β†’ 𝑝, 𝑏 : π‘Ÿ β†’ ¬𝑝}
                             𝐹4 = {π‘Ž : 𝑝, 𝑏 : π‘Ÿ β†’ 𝑝}
                             𝐹5 = {𝑏 : π‘Ÿ β†’ 𝑝, 𝑏 : π‘Ÿ β†’ ¬𝑝}
                             𝐹6 = {π‘Ž : ¬𝑝, 𝑏 : π‘Ÿ β†’ ¬𝑝}
                             𝐹7 = {π‘Ž : ¬𝑝, 𝑏 : π‘Ÿ β†’ 𝑝, 𝑏 : π‘Ÿ β†’ ¬𝑝}
                             𝐹8 = {π‘Ž : 𝑝, π‘Ž : ¬𝑝, 𝑏 : π‘Ÿ β†’ 𝑝, 𝑏 : π‘Ÿ β†’ ¬𝑝}


Using formula (5) one can cmput mc(𝐹𝑖 ) and then sum all the result, obtaining mc((2)). Let us
for instance compute mc(𝐹3 ) and mc(𝐹4 )

    mc(𝐹3 ) = (2π‘šπ‘π‘Ž (⊀) βˆ’ 2π‘šπ‘π‘Ž (𝑝) βˆ’ 2π‘šπ‘π‘Ž (¬𝑝) + 2π‘šπ‘π‘Ž (π‘βˆ§Β¬π‘) ) Β· 2π‘šπ‘π‘ ((π‘Ÿβ†’π‘)∧(π‘Ÿβ†’Β¬π‘))
             = 22 βˆ’ 21 βˆ’ 21 + 20 ) Β· 22                                                     =4
                   π‘šπ‘π‘Ž (𝑝)      π‘šπ‘π‘Ž (π‘βˆ§Β¬π‘)        π‘šπ‘π‘ (π‘Ÿβ†’π‘)        π‘šπ‘π‘ (π‘Ÿβ†’π‘βˆ§π‘Ÿβ†’Β¬π‘)
    mc(𝐹4 ) = (2             βˆ’2              ) Β· (2           βˆ’2                    )
             = (21 βˆ’ 20 ) Β· (23 βˆ’ 22 )                                                      =4


4. Conclusion and future directions
In this short note, we proved a formula to compute model counting for MC systems that is based
on model counting for each single context. This initial idea can be generalised in a number
of directions. The first direction concerns the generalisation to MC weighted model counting.
Weighted model counting is tightly connected to probabilistic reasoning (see e.g., [9]), this will
open the opportunity of doing contextual probabilistic inference. A second research direction
can be obtained by exploiting the correspondence between modal logic and MC systems proved
in [2] and develop a context based approach to model counting and probabilistic inference for
modal logic. Finally one could extend the result of this note to distributed first order logic [5]
and distributed description logics [6]. Further generalisation involves more complex bridge
rules including for instance negated labelled formulas and disjunction of labelled formulas.
References
[1] J. McCarthy, Notes on formalizing context, in: Proceedings of the 13th international joint
    conference on Artifical intelligence, 1993, pp. 555–560.
[2] F. Giunchiglia, L. Serafini, Multilanguage hierarchical logics, or: how we can do without
    modal logics, Artificial intelligence 65 (1994) 29–70.
[3] C. Ghidini, F. Giunchiglia, Local models semantics, or contextual reasoning= locality+
    compatibility, Artificial intelligence 127 (2001) 221–259.
[4] G. Brewka, T. Eiter, Equilibria in heterogeneous nonmonotonic multi-context systems, in:
    AAAI, volume 7, 2007, pp. 385–390.
[5] C. Ghidini, L. Serafini, Distributed first order logic, Artificial Intelligence 253 (2017) 1–39.
[6] A. Borgida, L. Serafini, Distributed description logics: Assimilating information from peer
    sources, in: Journal on data semantics I, Springer, 2003, pp. 153–184.
[7] A. Darwiche, Three modern roles for logic in ai, in: Proceedings of the 39th ACM SIGMOD-
    SIGACT-SIGAI Symposium on Principles of Database Systems, 2020, pp. 229–243.
[8] H. S. Wilf, Generatingfunctionology, A. K. Peters, Ltd., USA, 2006.
[9] M. Chavira, A. Darwiche, On probabilistic inference by weighted model counting, Artificial
    Intelligence 172 (2008) 772–799.