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.