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 multiple 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 |= +1
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
Ω = {Ω }∈ where
where is a sentential formula of . A model for an MCS ⟨︀ {Φ }∈ , BR⟩︀ is a structure
1. Ω is a set of interpretations of such that for all ∈ Ω , |= Φ (written as Ω |= Φ );
2. For every bridge rule of the form (
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:
(
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: 1When 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 ⊆ : 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)
=0
(
⃒⃒ ⃒⃒
∑⊆ ︁¯ ⃒⃒⃒⃒ ⋂∈︁ ⃒⃒⃒⃒
||=
Notice that Ω ∈ ⋂︀∈ if and only if Ω |= ∧ . This implies that ⃒⃒⃒ ⋂︀∈ ⃒⃒⃒ is the number
of subsets of the set of models that satisfiey ∧ , i.e.,
=
∑︁ 2(∧)
⊆ ¯
||=
0 =
∑︁ (− 1)||2(∪)
⊆ ¯
From which we conclude that the number of sets of models that satisfies and do not satisfy
¯ is:
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
∑︀⊆ ¯ (− 1)||2(∪) of such sets of models, we can conclude that
(
∏︁ ∑︁ (− 1)||2(∪) ∈F(BR) ⊆ ¯ Theorem 1.
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)
∑︁ ∈F(BR) ⊆ ¯ ∏︁ ∑︁ (− 1)||2(∪) □
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
(
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.