# forgetting_in_multiagent_modal_logics__0b8512fe.pdf

Forgetting in Multi-Agent Modal Logics

Liangda Fang1,3 Yongmei Liu1 Hans van Ditmarsch2

1Dept. of Computer Science, Sun Yat-sen University, Guangzhou 510006, China

2LORIA, CNRS Universit e de Lorraine, France 3Dept. of Computer Science, Jinan University, Guangzhou 510632, China fangld@jnu.edu.cn, ymliu@mail.sysu.edu.cn, hans.van-ditmarsch@loria.fr

In the past decades, forgetting has been investigated for many logics and has found many applications in knowledge representation and reasoning. However, forgetting in multi-agent modal logics has largely been unexplored. In this paper, we study forgetting in multi-agent modal logics. We adopt the semantic definition of existential bisimulation quantifiers as that of forgetting. We propose a syntactical way of performing forgetting based on the canonical formulas of modal logics introduced by Moss. We show that the result of forgetting a propositional atom from a satisfiable canonical formula can be computed by simply substituting the literals of the atom with >. Thus we show that Kn, Dn, Tn, K45n, KD45n and S5n are closed under forgetting, and hence have uniform interpolation.

1 Introduction

In the past decades, forgetting has been investigated for many logics and has found many applications in knowledge representation and reasoning (KR). Intuitively, forgetting some symbols from a knowledge base (KB) should result in a weaker KB which entails the same set of sentences that do not mention those symbols.

The seminal paper by Lin and Reiter [1994] studied forgetting in propositional and first-order logics. Over the years, forgetting in propositional logic has been used in abductive reasoning [Lin, 2001], reasoning under inconsistency [Lang and Marquis, 2010], reasoning about knowledge [Su et al., 2009], epistemic planning [Herzig et al., 2003], etc; and forgetting in first-order logic has been applied to progression for basic action theories in the situation calculus [Lin and Reiter, 1997; Liu and Lakemeyer, 2009]. In recent years, forgetting has been generalized to various description logics and applied to ontology reuse [Wang et al., 2009; 2010; Konev et al., 2009; Lutz and Wolter, 2011]. There exist some resolutionbased approaches for forgetting in expressive description logics [Ludwig and Konev, 2014; Koopmann and Schmidt, 2014; 2015]. Forgetting has also been studied for logic programs and used in conflict solving [Zhang and Foo, 2006; Eiter and Wang, 2008; Wang et al., 2014].

Forgetting for modal logics has also been investigated and applied to reasoning about knowledge and belief. Baral and Zhang [2005] studied knowledge update, a special form of update with the effect that the agent becomes ignorant of a propositional formula. Van Ditmarsch et al. [2009] presented a dynamic epistemic logic where the dynamic operator is the action of forgetting a propositional atom. Zhang and Zhou [2009] studied forgetting in propositional S5 logic and its applications in knowledge updates and knowledge games. Liu and Wen [2011] explored forgetting in first-order S5 logic and applied it to progression of knowledge in the situation calculus, which concerns updating the current representation of the world state and agents epistemic state to reflect the change caused by an ontic or epistemic action. Later, Fang et al. [2015] extended the above results to progression of both knowledge and belief for nondeterministic actions in the single-agent propositional case.

Zhang and Zhou s semantic definition of forgetting coincides with that of existential bisimulation quantifiers. Bisimulation quantifiers were introduced by Ghilardi and Zawadowski [1995] to study uniform interpolation, which is the dual notion of forgetting, in modal logics. A logic has uniform interpolation if for any formula φ and any set S of symbols occurring in φ, there is a formula using only symbols in S such that φ and entail the same set of sentences formulated only in S. The semantics of existential bisimulation quantifiers is as follows: a model M satisfies a formula 9pφ where p is an atom iff there is a model M 0 satisfying φ such that M and M 0 are bisimilar with exception on p. It turns out that any logic that is invariant under bisimulation and closed under bisimulation quantification, that is, closed under elimination of the quantification, has uniform interpolation. It is well-known that K, T and S5 have uniform interpolation [Ghilardi, 1995; B ılkov a, 2007; Ghilardi and Zawadowski, 2000]. However, neither K4 or S4 has uniform interpolation [B ılkov a, 2007; Ghilardi and Zawadowski, 1995].

In the multi-agent case, D Agostino and Lenzi [2006] gave a constructive proof that µ-calculus, an extension of Kn with a fixed-point operator, is closed under bisimulation quantification and hence has uniform interpolation. Studer [2009] showed that KC, which is Kn with common knowledge, does not have uniform interpolation, and this also holds for K4C. Pattinson [2013] showed that all modal logics axiomatizable

Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI-16)

by formulas whose modal depth uniformly equals one, including Kn and Dn, have uniform interpolation. Reasoning about knowledge and belief in the multi-agent case is certainly important from the KR point of view, since higherorder knowledge and belief (i.e., knowledge and belief about other agents knowledge and belief) play an important role in coordination and interaction. However, to the best of our knowledge, other than the above mentioned works, forgetting in multi-agent modal logics has largely been unexplored, and it remains an open problem whether Tn, K45n, KD45n or S5n have uniform interpolation.

It is well-known that in propositional logic, the result of forgetting atom p from a satisfiable term (i.e., a conjunction of literals) δ can be obtained from δ by substituting any occurrence of literal p or p with >. As every propositional formula can be equivalently transformed into a disjunction of satisfiable terms, and forgetting is distributive over disjunction, propositional logic is closed under forgetting. Interestingly, the idea of literal elimination was used by D Agostino and Lenzi to prove that µ-calculus is closed under bisimulation quantification.

In this paper, we study forgetting in multi-agent modal logics. We adopt the semantic definition of existential bisimulation quantifiers as that of forgetting. We resort to the normal forms of propositional modal logics, called canonical formulas by Moss [2007], a nice property of which is that an arbitrary modal formula is equivalent to a disjunction of a finite set of satisfiable canonical formulas. Due to the distributive law of forgetting over disjunction, forgetting from arbitrary modal formulas can be reduced to forgetting from satisfiable canonical formulas, which we show can be computed via literal elimination. Hence we show that except K4n and S4n, which do not have uniform interpolation, the other main multi-agent modal systems are closed under forgetting.

2 Preliminaries In this section, we introduce the background material, i.e., the syntax and semantics of multi-agent modal logics, and the canonical formulas for modal logics as defined by Moss.

2.1 Multi-agent modal logics We fix a set A of n agents and a countable set of atoms P.

Definition 1 The language LK

n is generated by the BNF:

φ ::= p | φ | φ φ | Kiφ,

where p 2 P and i 2 A. We use Lpl for the propositional language, i.e., the language without the Ki modality.

We let > and ? represent true and false respectively. We use p and q to range over atoms, φ and to range over formulas, and Φ and to range over sets of formulas. We let P(φ) denote the set of atoms which appear in φ.

The (modal) depth of a formula φ in LK

n , written dep(φ), is the depth of nesting of modal operators in φ. We let ˆKiφ stand for Ki φ. We let W Φ (resp. V Φ) denote the disjunction (resp. conjunction) of members of Φ; and we use V ˆKiΦ to represent the conjunction of ˆKiφ where φ 2 Φ.

Definition 2 A frame is a pair (S, R), where

L K D T K4 S4 K45 KD45 S5 Serial X X X X X Reflexive X X X Transitive X X X X X Euclidean X X X

Table 1: The main modal systems

S is a non-empty set of possible worlds;

For each agent i 2 A, Ri is a binary relation on S, called

the accessibility relation for i.

For s 2 S, we write Ri(s) for {t 2 S | s Rit}, and call it the i-children of s.

Different modal systems result from different sets of conditions on the accessibility relations. We say Ri is serial if for any s 2 S, there is s0 2 S s.t. s Ris0; we say Ri is Euclidean if whenever s Ris1 and s Ris2, we have s1Ris2.

We list the main modal systems in Table 1. KD45 and S5 are well-accepted as the logics for knowledge and belief, respectively. For each symbol L listed here, we use L for the single agent case, Ln for the case where there are n agents.

Definition 3 A Kripke model is a triple M = h S, R, V i, where (S, R) is a frame, and V is a valuation map, which maps each s 2 S to a subset of P. A pointed Kripke model is a pair (M, s), where M is a Kripke model and s is a world of M, called the actual world.

For simplicity, we often omit the word pointed .

Definition 4 Let (M, s) be a Kripke model where M = h S, R, V i. We interpret formulas in LK

n by induction:

M, s |= p iff p 2 V (s);

M, s |= φ iff M, s 6|= φ;

M, s |= φ iff M, s |= φ and M, s |= ;

M, s |= Kiφ iff for all t 2 Ri(s), M, t |= φ.

We use L to range over modal systems. Consider the context of a modal system L. We say φ is satisfiable, if there exists a model of φ. We say φ entails , written φ |= , if for any model (M, s), M, s |= φ implies M, s |= . We say φ and are equivalent, written φ , if φ |= and |= φ.

D Agostino and Lenzi [2005] presented another modal language which is based on the cover modality ri:

Definition 5 Let i 2 A, and Φ a finite set of formulas in LK

n . We use riΦ to denote the formula Ki(W Φ) (V ˆKiΦ).

Note that ri; Ki?.

Now, we can get the semantics of the cover modality.

Lemma 1 Let (M, s) be a Kripke model where M = h S, R, V i and s 2 S. Then M, s |= riΦ iff the following conditions hold:

for all t 2 Ri(s), there is φ 2 Φ s.t. M, t |= φ;

for all φ 2 Φ, there is t 2 Ri(s) s.t. M, t |= φ.

Proposition 1 [Janin and Walukiewicz, 1995] Every formula in LK

n is equivalent to a formula using only the ri modalities.

2.2 Canonical formulas We will present our definitions and proofs via canonical formulas of modal logics, as defined by Moss [2007], which capture Kripke models up to a given depth.

Definition 6 (Canonical formulas) Let P P be finite. We inductively define the set EP

k as follows:

p2P \ P p | P P};

k+1 = {δ0 V

i2A riΦi | δ0 2 EP

0 and Φi EP

Let δ = δ0 V

i2A riΦi 2 EP

k+1. We denote δ0 by w(δ), and call it the world of δ; we denote Φi by Ri(δ), and call it the i-children of δ.

Intuitively, when we restrict our attention to the atoms in P, a canonical formula of depth k provides a complete syntactic representation of a Kripke model up to depth k.

The following proposition says that every Kripke model (M, s) satisfies a unique canonical formula of a given depth k, which we call the depth k canonical formula of (M, s).

Proposition 2 [Moss, 2007] Let (M, s) be a model and k 2 N. Let P P be finite. Then, there exists a unique δ 2 EP

k s.t. M, s |= δ.

We can get the following corollary which means that every modal formula can be equivalently transformed into a disjunction of satisfiable canonical formulas whose depth is not less than that of the original formula.

Proposition 3 Consider the context of a modal system L. Let φ 2 LK

n and l 2 N s.t. l dep(φ). Let P = P(φ). Then there exists a unique set Φ EP

l s.t. φ W Φ, and for every δ 2 Φ, δ is satisfiable in L.

Now, we introduce the projection operations on canonical formulas. A canonical formula can be graphically represented as a tree. The operation δ# prunes the leaves of this tree. In δ#l, we perform pruning l times sequentially. We call δ# the 1st-cut of δ, and δ#l the lth-cut of δ.

Definition 7 Let P P be finite. Let k 2 N and δ 2 EP

k . Then, δ# is inductively defined as follows:

δ, if k = 0; w(δ), if k = 1; w(δ) V

i2A ri(Ri(δ))#, otherwise.

Let Φ be a set of canonical formulas. We use Φ# to denote the set {φ# | φ 2 Φ}.

Definition 8 Let P P be finite. Let k, l 2 N s.t. k l. Let δ 2 EP

k . Then, δ#l is inductively defined as follows:

δ, if l = 0; δ#, if l = 1; (δ#l 1)#, otherwise.

Similarly to Φ#, Φ#l is the set {φ#l | φ 2 Φ}. Obviously, δ |= δ#l for all l dep(δ).

It is easy to prove the following, which intuitively says that the i-children of the lth-cut of a canonical formula is equal to the lth-cut of its i-children, i.e., the two operations are commutative.

Proposition 4 Let δ be a canonical formula. Let l 2 N s.t. l < dep(δ). Then for all i 2 A, we have Ri(δ#l) = Ri(δ)#l.

Example 1 Let δ = p ri{ p ri{p, p}}. Obviously, the depth of δ is 2. By Definitions 7 and 8, δ#1 = δ# = p ri({ p ri{p, p}})# = p ri{ p}. Similarly, we get Ri(δ#1) = { p}, Ri(δ) = { p ri{p, p}}, and Ri(δ)#1 = { p}. Hence Ri(δ#1) = Ri(δ)#1 = { p}.

3 Forgetting

In this section, we define forgetting in multi-agent modal logics. We first review forgetting in propositional logic.

We use a subset of the atoms to denote a valuation.

Definition 9 Let φ 2 Lpl and p an atom. A formula 2 Lpl s.t. P( ) P(φ)\{p} is a result of forgetting p in φ, written pforget(φ, p) , if for any valuation P, P |= φ (meaning P satisfies φ) iff there is a valuation P 0 s.t. P 0 |= and P p P 0, i.e., P \ {p} = P 0 \ {p}.

The definition of forgetting in multi-agent modal logics is analogous to that in propositional logic. For this purpose, we use the well-known concept of bisimulation.

Definition 10 (p-bisimulation) Let (M, s) and (M 0, s0) be two Kripke models where M = h S, R, V i and M 0 = h S0, R0, V 0i. A p-bisimulation between (M, s) and (M 0, s0) is a relation S S0 s.t. s s0, and whenever t t0, we get:

atoms V (t) p V 0(t0);

forth For all i, if t Riu, then there is u0 s.t. t0R0

iu0 and u u0;

back For all i, if t0R0

iu0, then there is u s.t. t Riu and u u0.

We say that (M, s) and (M 0, s0) are p-bisimilar, written (M, s)$p(M 0, s0), if there is a p-bisimulation between them.

Clearly, $p is an equivalence relation. A nice property of p-bisimilar Kripke models is that they agree on all modal formulas wherein p does not appear.

Proposition 5 Let (M, s)$p(M 0, s0). Let φ 2 LK

n where p does not appear in φ. Then M, s |= φ iff M 0, s0 |= φ.

Definition 11 (Forgetting) Consider the context of a modal system L. Let φ 2 LK

n and p an atom. A formula s.t. P( ) P(φ) \ {p} is a result of forgetting p in φ, written kforget(φ, p) , if for any model (M 0, s0), M 0, s0 |= iff there is a model (M, s) of φ s.t. (M, s)$p(M 0, s0).

So the semantics of forgetting is that of existential bisimulation quantifiers as presented in the introduction. Clearly, if both 1 and 2 are results of forgetting p in φ, then they are logically equivalent. In this paper, when we prove kforget(φ, p) , the proof of the if direction of Definition 11 is straightforward by making use of (M, s)$p(M 0, s0) and the induction hypothesis if applicable. To save space, we only present the proof of the only-if direction.

We now analyze basic properties of forgetting.

Proposition 6 Consider the context of a modal system L. If kforget(φ, p) , then φ |= ; and for any where p does not occur, φ |= iff |= .

Proposition 7 Consider the context of a modal system L.

1. If φ 2 Lpl and pforget(φ, p) , then kforget(φ, p)

2. kforget(φ1 _ φ2, p) kforget(φ1, p) _ kforget(φ2, p).

Proof: We only prove the only-if direction of Part 1. Let M 0, s0 |= . We let the structure of M be a copy of that of M 0; let V expand V 0 s.t. V (s) |= φ. Then we have M, s |= φ and (M, s)$p(M 0, s0).

We now relate forgetting to uniform interpolation.

Definition 12 We say that a modal system L is closed under forgetting if for any formula φ and any atom p 2 P(φ), there exists an L formula s.t. kforget(φ, p) .

Definition 13 We say a modal system L has uniform interpolation if for every formula φ and every P P(φ), there is a formula such that P( ) P and such that for any formula with P( ) P, we have φ |= iff |= .

Zhang and Zhou [2009] proposed the forgetting postulates, which correspond to the definition of uniform interpolation.

By Proposition 6, we have

Proposition 8 If a modal system L is closed under forgetting, then L has uniform interpolation.

As mentioned in the introduction, neither K4 nor S4 has uniform interpolation. Because K4 is indeed K41, which is a special case of K4n, K4n does not have uniform interpolation. Similarly, neither has S4n. Hence, we get

Corollary 1 Neither K4n nor S4n is closed under forgetting.

Finally, we propose a syntactical method of forgetting.

Definition 14 (Literal elimination) Let φ 2 LK

n and p an atom. We let φp denote the formula obtained from φ by substituting all occurrences of p with > and subsequently substituting all occurrences of p with >.

Merely requiring to replace p and p by > would be ambiguous. Because, should we then replace p by > or by ?? The last would happen if we were to replace the p in p by >. That would be an undesirable outcome. The subsequently in Definition 14 is not ambiguous and avoids that outcome.

Example 2 Let δ1 = p q ri{ p q}. Then, δp

1 = > q ri{> q} q ri{ q}.

Typically, we only apply this substitution to formulas wherein negations only bind atoms. Similarly to Φ#, Φp is the set {φp | φ 2 Φ}.

In the following sections, we will show that when δ is a canonical formula satisfiable in L, kforget L(δ, p) δp.

4 Forgetting in multi-agent modal logics

In this section, we show that forgetting from satisfiable canonical formulas can be computed via literal elimination in the following multi-agent modal logics: Kn, Dn, Tn, K45n, KD45n and S5n. As an easy corollary, we have that the above logics are closed under forgetting and they have uniform interpolation.

Figure 1: Illustration for the proof of Theorem 1

4.1 Forgetting in Kn and Dn In this subsection, we consider Kn and Dn cases. In fact, these results were first proved by D Agostino and Lenzi [2006]. As mentioned in the introduction, they gave a constructive proof that µ-calculus is closed under bisimulation quantification. The core result they proved is the following: Theorem [D Agostino and Lenzi, 2006] Let φ be a cover disjunctive formula for µ-calculus. Then 9pφ φp.

In the theorem, a cover disjunctive formula is a generalization of the notion of a disjunction of canonicial formulas that we use in this paper.

Here 9p is the bisimulation quantifier we defined in the introduction. Their proof is via an automata approach. Here we present an easy inductive proof, which serves as the basis for the proofs of all the forgetting results in this paper.

Theorem 1 (The basic theorem) Let L be Kn or Dn, and δ an L-satisfiable canonical formula. Then kforget L(δ, p) δp.

Proof: We prove by induction on dep(δ). The base case, i.e., δ 2 EP

0 , follows from Proposition 7. We prove the only-if direction of the induction case, i.e., δ 2 EP

k where k 1. Let M 0, s0 |= δp. We construct M and define a relation between the worlds of M and M 0 as follows. Figure 1 illustrates the construction.

1. Create a new world s, let s s0, and V (s) |= w(δ). 2. For all i 2 A, t0 2 R0

i(s0), and 2 Ri(δ), if M 0, t0 |= p, by the induction hypothesis, there exist (Mt0, , tt0, ) and t0, s.t. Mt0, , tt0, |= and t0, : (Mt0, , tt0, )$p(M 0, t0). Add a new copy of Mt0, into M, let s Ritt0, , and expand with t0, . It is easy to show that : (M, s)$p(M 0, s0) and M, s |= δ.

In the case of Dn, it is obvious from the above construction that if M 0 satisfies seriality, so does M.

As a corollary of Propositions 3, 7 and Theorem 1, we get Corollary 2 Kn and Dn are closed under forgetting.

Example 3 Let φ be ˆKip ˆKi p, meaning that agent i is ignorant about p. Intuitively, after forgetting p, the agent should still have consistent belief. We convert φ into a disjunction of two canonical formulas δ1 and δ2 where δ1 = p ri{p, p} and δ2 = p ri{p, p}. Then δp

2 = > ri{>}. The disjunction of them is equivalent to ˆKi>.

4.2 Forgetting in Tn

In this subsection, we analyze properties of Tn satisfiable canonical formulas, and show that forgetting via literal elimination applies to them.

We begin with a simple example which shows that Theorem 1 does not hold for unsatisfiable canonical formulas.

Example 4 Let δ = p ri{p}. Clearly, δ is a canonical formula, and it is equivalent to ? in Tn. However, δp = > ri{>} which is equivalent to >.

The reason that forgetting via literal elimination does not work on δ is that δ is unsatisfiable in Tn. This motivates us to consider only satisfiable canonical formulas.

The following proposition says that any Tn satisfiable canonical formula δ has the reflexive property: for any agent i and any 1 l dep(δ), the lth-cut of δ is an i-child of its (l 1)th-cut.

Proposition 9 Let δ be a Tn satisfiable canonical formula where dep(δ) 1. Let l 2 N s.t. 1 l dep(δ). Then, for all i 2 A, we have δ#l 2 Ri(δ#l 1).

Proof: Here, we only prove the base case, i.e., δ# 2 Ri(δ). Let k = dep(δ) and M, s |= δ. Obviously, M, s |= δ#. Since M is reflexive, s 2 Ri(s). By the semantics of the ri modality, there exists δi 2 Ri(δ) s.t. M, s |= δi. So both δ# and δi are the depth k 1 canonical formula of (M, s) (cf. Proposition 2). Hence δ# = δi 2 Ri(δ).

Example 4 Cont d We have δ# = p and Ri(δ) = {p}. Obviously, δ# /2 Ri(δ). So δ is not satisfiable in Tn.

Example 5 Let δ = p q ri{p q, p q}. It is a Tn satisfiable canonical formula. Then, δ# = p q, and Ri(δ) = {p q, p q}. Obviously, δ# 2 Ri(δ).

Theorem 2 (The Tn theorem) Let δ be a Tn satisfiable canonical formula. Then kforget Tn(δ, p) δp.

Proof: The proof is the same as that of the basic theorem except the following. In the induction case, we get (M, s)$p(M 0, s0) and M, s |= δ. Let k = dep(δ). Then for any l k, M, s |= δ#l. We now let s Ris for each agent i. It is obvious that (M, s) is a Tn model. It is easy to see that (M, s)$p(M 0, s0) still holds. It remains to show that M, s |= δ still holds. We prove by induction on k l that for any l k, M, s |= δ#l still holds. Base case. M, s |= w(δ), which is δ#k. Induction case. Suppose that M, s |= δ#l. To show that M, s |= δ#l 1, it suffices to show that for each i 2 A, there exists 2 Ri(δ#l 1) s.t. M, s |= . By Proposition 9, δ#l 2 Ri(δ#l 1). Hence δ#l is the desired .

4.3 Multi-pointed Kripke models

In the next subsection, we show that forgetting via literal elimination applies to satisfiable canonical formulas of K45n, KD45n and S5n. The proof for the basic theorem does not immediately carry forward to these cases, because the model constructed in the proof may not be transitive or Euclidean. Also, we cannot simply fix the problem by adding edges as we do in the proof of the Tn theorem. We will overcome the problem via multi-pointed Kripke models which offers flexibility in the construction of required models. In this subsection, we introduce the basic concepts regarding multi-pointed models.

Definition 15 A multi-pointed Kripke model is a pair (M, T) where M is a Kripke model, and T is a possibly empty set of worlds of M.

Throughout this paper, we use (M, s) to denote a singlepointed model, and (M, T) a multi-pointed model.

Given a single-pointed model (M, s) and i 2 A, we can naturally obtain a multi-pointed model (M, T) where T = Ri(s), i.e., the i-children of s.

Similarly to the semantics of the cover modality, we have:

Definition 16 Let Φ be a set of formulas. We say a multipointed model (M, T) is Φ-complete if the following hold:

for every t 2 T, there exists φ 2 Φ s.t. M, t |= φ;

for every φ 2 Φ, there exists t 2 T s.t. M, t |= φ.

Obviously, M, s |= riΦ iff (M, Ri(s)) is Φ-complete. Then, we can extend Proposition 2 to multi-pointed models: we have that a multi-pointed model (M, T) corresponds to a unique set of canonical formulas of a given depth k, which we call the depth k canonical formula set of (M, T).

Proposition 10 Let (M, T) be a multi-pointed model, and k 2 N. Let P P be finite. Then, there exists a unique set Φ EP

k s.t. (M, T) is Φ-complete.

We now extend the concept of bisimulation to multipointed models.

Definition 17 Let (M, T) and (M 0, T 0) be two Kripke models. A p-bisimulation between (M, T) and (M 0, T 0) is a relation between the worlds of M and M 0 s.t.

for every t 2 T, there exists t0 2 T 0 s.t. t t0;

for every t0 2 T 0, there exists t 2 T s.t. t t0;

whenever u u0, the atoms, forth and back conditions in

Definition 10 hold.

We end with a constraint on multi-pointed models, which is crucial for constructing transitive and Euclidean models.

Definition 18 Let (M, T) be a Kripke model and i 2 A. We say that (M, T) is i-equivalent if for all t1, t2 2 T, we have t1Rit2, and for every s 2 S, if there exists t 2 T s.t. s Rit or t Ris, then s 2 T.

4.4 Forgetting in K45n, KD45n and S5n In this subsection, we generalize the forgetting results for satisfiable canonical formulas to K45n, KD45n and S5n.

The following proposition says that any K45n satisfiable canonical formula δ has the identical-children property: for any agent i and any i-child δi of δ, the lth-cut of δ s i-children is equal to the i-children of the (l 1)th-cut of δi.

Proposition 11 Let δ be a K45n satisfiable canonical formula where dep(δ) 2. Let l 2 N s.t. 1 l < dep(δ). Then, for all i 2 A and δi 2 Ri(δ), (Ri(δ))#l = Ri(δ#l 1

Proof: Let k = dep(δ), M, s |= δ, i 2 A and δi 2 Ri(δ). Here, we only prove the base case, i.e., (Ri(δ))# = Ri(δi). Then there exists t 2 Ri(s) s.t. M, t |= δi. Since M is transitive and Euclidean, Ri(s) = Ri(t). Obviously, (M, Ri(s)) is (Ri(δ))#-complete and (M, Ri(t)) is Ri(δi)-complete. So (M, Ri(s)) is also Ri(δi)-complete. So both (Ri(δ))# and Ri(δi) are the depth k 2 canonical formula set of (M, Ri(s)) (cf. Proposition 10). Hence (Ri(δ))# = Ri(δi).

Now, we prove an important lemma, which is the multipointed extension of the only-if direction of the version of the basic theorem for K45n.

Lemma 2 (The K45n lemma) Let δ be a K45n satisfiable canonical formula where dep(δ) 1. Let (M 0, s0) be a K45n model of δp. Then for all i 2 A, there exists a multi-pointed K45n model (M, T) that is i-equivalent, Ri(δ)-complete and (M, T)$p(M 0, R0

Proof: We prove by induction on dep(δ).

Base case, i.e., Ri(δ) is a set of propositional formulas. We construct (M, T) and define the p-bisimulation between (M, T) and (M 0, R0

i(s0)) as follows. Figure 2 illustrates the construction. We initialize S = ; and = ;.

1. For all t0 2 R0

i(s0) and δi 2 Ri(δ), if M 0, t0 |= δp

i , we create a world t s.t. V (t) |= w(δi). Then we add it into S and T, and let t t0. 2. For all t1, t2 2 T, we let t1Rit2. 3. For t 2 T and j 6= i, we make a copy of (M 0, R0

j(t0)), denoted by (Mt,j, Tt,j) where t0 is the original world of t. We connect t to all worlds of Tt,j via j-edges, i.e., let t Rju for u 2 Tt,j. We let u u0 when u is the copy of u0. It is easy to verify (M, T) satisfies the requirements.

Induction step. The construction of (M, T) is similar to that of the base case except the following. In Step 3, since M 0, t0 |= δp

i , by the induction hypothesis, there exist (Mt,j, Tt,j) that is j-equivalent and Rj(δi)-complete and t,j: (Mt,j, Tt,j)$p(M 0, R0

j(t0)). We expand with t,j. Obviously, (M, T) is transitive, Euclidean and i-equivalent, and (M, T)$p(M 0, R0

i(s0)). It remains to verify that (M, T) is Ri(δ)-complete. Let dep(δ) = k. We prove by induction on k l that for all 0 l < k, (M, T) is Ri(δ)#l-complete. Base case: l = k 1, and Ri(δ)#l is a set of propositional formulas. By Step 1, (M, T) is Ri(δ)#l-complete. Induction step. Suppose that (M, T) is Ri(δ)#l-complete. We prove that it is also (Ri(δ))#l 1-complete. Let t 2 T. By the construction, there exists δi 2 Ri(δ) s.t. M, t |= w(δi). It

Figure 2: Illustration for the proof of Lemma 2

suffices to show that M, t |= δ#l 1

i . Since w(δ#l 1

i ) = w(δi), M, t |= w(δ#l 1

i ). By the identical-children property (Proposition 11), (Ri(δ))#l = Ri(δ#l 1

i ). By the induction hypothesis, (M, T) is Ri(δ#l 1

i )-complete, so M, t |= ri Ri(δ#l 1

i ). For j 6= i, because (Mt,j, Tt,j) is Rj(δi)- complete and Rj(t) = Tt,j, M, t |= rj Rj(δi), hence M, t |= rj Rj(δi)#l 1. By Proposition 4, Rj(δi)#l 1 = Rj(δ#l 1

i ), so M, t |= rj Rj(δ#l 1

Now, we get the following theorem via Lemma 2.

Theorem 3 (The K45n theorem) Let δ be a K45n satisfiable canonical formula. Then kforget K45n(δ, p) δp.

Proof: The proof is the same as that of the basic theorem except Step 2 of the induction case. By the K45n lemma, for every i 2 A, there exist (Mi, Ti) and i : (Mi, Ti)$p(M 0, R0

i(s0)). Add a new copy of Mi into M, let s Rit for all t 2 Ti, and expand with i.

From the construction of the K45n lemma and the K45n theorem, if the given model M 0 is a KD45n model, then we can acquire a KD45n model M. Hence we can get

Theorem 4 Let δ be a KD45n satisfiable canonical formula. Then kforget KD45n(δ, p) δp.

We proceed to S5n. The models constructed in the proofs of the K45n lemma and the K45n theorem may not be reflexive. We can fix it via adding edges as follows: for all i 2 A,

1. for all t 2 S, we let t Rit; (reflexive edges)

2. for all t, u 2 S, if t Riu, we let u Rit. (symmetric edges)

It is easy to verify that the new models are S5n models.

Example 6 In Figure 3, given a model (M, T) shown in Figure 2, we add blue edges so that it is an S5n model. Note that it is not necessary to add edges for four submodels (Mt1,j, Tt1,j), (Mt1,k, Tt1,k), (Mt2,j, Tt2,j) and

Figure 3: Adding reflexive and symmetric edges

(Mt2,k, Tt2,k). All of them are S5n models since they are acquired by the induction hypothesis. We just add the edges as follows:

1. Let t1Rjt1, t1Rkt1, t2Rjt2 and t2Rkt2; 2. For u 2 Tt1,j (resp. Tt1,k), let u Rjt1 (resp. u Rkt1). 3. For u 2 Tt2,j (resp. Tt2,k), let u Rjt2 (resp. u Rkt2).

All that remains now is to prove that the constructed models satisfy the original formulas. Since the logic S5n is both K45n and Tn logics, any S5n satisfiable canonical formula has the reflexive and identical-children properties (Propositions 9 and 11). Hence, we get

Theorem 5 (The S5n theorem) Let δ be an S5n satisfiable canonical formula. Then kforget S5n(δ, p) δp.

Proof: Let k = dep(δ). Here, we only verify that M, s |= δ when k 1. We prove by induction on k l that for any l k, M, s |= δ#l still holds. Base case. M, s |= w(δ), which is δ#k. Induction case. Suppose that M, s |= δ#l. To show that M, s |= δ#l 1, it suffices to show that for each i 2 A, M, s |= ri Ri(δ#l 1), i.e., (M, Ri(s)) is Ri(δ#l 1)- complete. Here, we only prove that for every t 2 Ri(s), there exists 2 Ri(δ#l 1) s.t. M, t |= . The other direction can be similarly proved.

Suppose that t = s. By the reflexive property, δ#l 2 Ri(δ#l 1). Let = δ#l. This, together with the hypothesis, imply that M, s |= where 2 Ri(δ#l 1).

Suppose that t 2 S \ {s}. Before adding the edges, by construction, there exists δi 2 Ri(δ) s.t. M, t |= δi. Let = δ#l 1

i . After adding the edges, that M, t |= w( ) V

j2A\{i} rj Rj( ) holds. Now, we prove that M, t |= ri Ri( ), i.e., (M, Ri(t)) is Ri( )-complete. By transitive and Euclidean properties, we get Ri(t) = Ri(s). By the identical children property, Ri( ) = Ri(δ#l). These, together with the hypothesis, imply that M, t |= ri Ri( ).

As a corollary of Theorems 2-5, we get

Corollary 3 Tn, K45n, KD45n and S5n are closed under forgetting.

By Proposition 8 and Corollary 3, we can get the next corollary which settles the open problems regarding uniform interpolation in multi-agent modal logics.

Corollary 4 Tn, K45n, KD45n and S5n do have uniform interpolation.

5 Conclusions

In this paper, we have studied forgetting in multi-agent modal logics. We adopted the semantic definition of existential bisimulation quantifiers as that of forgetting. We showed that except the two modal systems K4n and S4n, which have been shown lack of uniform interpolation, the other main multiagent modal systems, namely Kn, Dn, Tn, K45n, KD45n, and S5n, are closed under forgetting.

To achieve the above results, we presented a syntactical method of forgetting: to forget an atom from an arbitrary modal formula, first transform the formula to a disjunction of canonical formulas, then remove all the unsatisfiable ones, and lastly substitute any literal of the atom with >. To prove that this syntactical method of forgetting produces the desired result, given a model satisfying the formula obtained from a satisfiable canonical formula via literal elimination, we construct a model satisfying the original formula and p-similar to the given model. To this end, we analyze properties of satisfiable canonical formulas in different logics, and use multipointed models to gain flexibility in model construction.

In multi-agent systems, background information is formalized as common knowledge of propositional formulas. We have also shown that the extensions of the above logics with propositional common knowledge are closed under forgetting. These results were omitted for lack of space.

It is well-known that the size of a canonical formula is nonelementary. So the proposed syntactic method of forgetting is obviously an unpractical one. Thus one topic for future research is to investigate more efficient approaches for computing forgetting. Yet another one is to explore forgetting for distributed knowledge and more general cases of common knowledge. It would also be interesting to apply forgetting to progression and abductive reasoning of knowledge and belief in multi-agent systems.

Acknowledgments

Liangda Fang and Yongmei Liu acknowledge support from the Natural Science Foundation of China under Grant Nos. 61572535 and 61573386. Hans van Ditmarsch acknowledges support from ERC project EPS313360. He is also affiliated to IMSc (Institute of Mathematical Sciences), Chennai, India, and to Zhejiang University, China.

[Baral and Zhang, 2005] Chitta Baral and Yan Zhang. Knowledge

updates: Semantics and complexity issues. Artificial Intelligence, 164(1-2):209 243, 2005.

[B ılkov a, 2007] Marta B ılkov a. Uniform Interpolation and Propo-

sitional Quantifiers in Modal Logics. Studia Logica, 85(1):1 31, 2007.

[D Agostino and Lenzi, 2005] Giovanna D Agostino and Giacomo

Lenzi. An axiomatization of bisimulation quantifiers via the µcalculus. Theoretical Computer Science, 338(1):64 95, 2005.

[D Agostino and Lenzi, 2006] Giovanna D Agostino and Giacomo

Lenzi. On modal µ-calculus with explicit interpolants. Journal of Applied Logic, 4(3):256 278, 2006.

[Eiter and Wang, 2008] Thomas Eiter and Kewen Wang. Seman-

tic forgetting in answer set programming. Artificial Intelligence, 172(14):1644 1672, 2008.

[Fang et al., 2015] Liangda Fang, Yongmei Liu, and Ximing Wen.

On the Progression of Knowledge and Belief for Nondeterministic Actions in the Situation Calculus. In Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI-2015), pages 2955 2963, 2015.

[Ghilardi and Zawadowski, 1995] Silvio Ghilardi and Marek W.

Zawadowski. A sheaf representation and duality for finitely presenting heyting algebras. Journal of Symbolic Logic, 60(3):911 939, 1995.

[Ghilardi and Zawadowski, 2000] Silvio Ghilardi and Marek W.

Zawadowski. From Bisimulation Quantifiers to Classifying Toposes. In Proceedings of the Third Workshop on Advances in Modal Logic (Ai ML-2000), volume 3, pages 193 220, 2000.

[Ghilardi, 1995] Silvio Ghilardi. An algebraic theory of normal forms. Annals of Pure and Applied Logic, 71(3):189 245, 1995.

[Herzig et al., 2003] Andreas Herzig, J erˆome Lang, and Pierre

Marquis. Action representation and partially observable planning using epistemic logic. In Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence (IJCAI-2003), pages 1067 1073, 2003.

[Janin and Walukiewicz, 1995] David Janin and Igor Walukiewicz.

Automata for the modal µ-calculus and related results. In Proceedings of the Twentieth International Symposium on Mathematical Foundations of Computer Science (MFCS-1995), pages 552 562, 1995.

[Konev et al., 2009] Boris Konev, Dirk Walther, and Frank Wolter.

Forgetting and Uniform Interpolation in Large-Scale Description Logic Terminologies. In Proceedings of the Twenty-First International Joint Conference on Artificial Intelligence (IJCAI-2009), pages 830 835, 2009.

[Koopmann and Schmidt, 2014] Patrick Koopmann and Renate A.

Schmidt. Count and Forget: Uniform Interpolation of SHQOntologiess. In Proceedings of Seventh International Joint Conference on Automated Reasoning (IJCAR-2014), pages 434 448, 2014.

[Koopmann and Schmidt, 2015] Patrick Koopmann and Renate A.

Schmidt. Uniform Interpolation and Forgetting for ALC Ontologies with ABoxes. In Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI-2015), pages 175 181, 2015.

[Lang and Marquis, 2010] J erˆome Lang and Pierre Marquis. Rea-

soning under inconsistency: A forgetting-based approach. Artificial Intelligence, 174(12-13):799 823, 2010.

[Lin and Reiter, 1994] Fangzhen Lin and Raymond Reiter. Forget

It! In Proceedings of AAAI Fall Symposium on Relevance, pages 154 159, 1994.

[Lin and Reiter, 1997] Fangzhen Lin and Raymond Reiter. How to progress a database. Artificial Intelligence, 92(1-2):131 167, 1997. [Lin, 2001] Fangzhen Lin. On strongest necessary and weakest sufficient conditions. Artificial Intelligence, 128(1-2):143 159, 2001. [Liu and Lakemeyer, 2009] Yongmei Liu and Gerhard Lakemeyer.

On First-Order Definability and Computability of Progression for Local-Effect Actions and Beyond. In Proceedings of the Twenty-First International Joint Conference on Artificial Intelligence (IJCAI-2009), pages 860 866, 2009. [Liu and Wen, 2011] Yongmei Liu and Ximing Wen. On the Pro-

gression of Knowledge in the Situation Calculus. In Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence (IJCAI-2011), pages 976 982, 2011. [Ludwig and Konev, 2014] Michel Ludwig and Boris Konev. Prac-

tical Uniform Interpolation and Forgetting for ALC TBoxes with Applications to Logical Difference. In Proceedings of the Fourteenth International Conference on Principles of Knowledge Representation and Reasoning (KR-2014), pages 318 327, 2014. [Lutz and Wolter, 2011] Carsten Lutz and Frank Wolter. Founda-

tions for Uniform Interpolation and Forgetting in Expressive Description Logics. In Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence (IJCAI-2011), pages 989 995, 2011. [Moss, 2007] Lawrence S. Moss. Finite models constructed from

canonical formulas. Journal of Philosophical Logic, 36(6):605 640, 2007. [Pattinson, 2013] Dirk Pattinson. The Logic of Exact Covers: Com-

pleteness and Uniform Interpolation. In Proceedings of the Twenty-Eighth ACM/IEEE Symposium on Logic in Computer Science (LICS-2013), pages 418 427, 2013. [Studer, 2009] Thomas Studer. Common knowledge does not have

the beth property. Information Processing Letters, 109(12):611 614, 2009. [Su et al., 2009] Kaile Su, Abdul Sattar, Guanfeng Lv, and Yan

Zhang. Variable Forgetting in Reasoning about Knowledge. Journal of Artificial Intelligence Research, 35(2):677 716, 2009. [van Ditmarsch et al., 2009] Hans van Ditmarsch, Andreas Herzig,

J erˆome Lang, and Pierre Marquis. Introspective forgetting. Synthese, 169(2):405 423, 2009. [Wang et al., 2009] Kewen Wang, Zhe Wang, Rodney Topor, Jeff Z. Pan, and Grigoris Antoniou. Concept and role forgetting in ALC ontologies. In Proceedings of the Eighth International Semantic Web Conference (ISWC-2009), pages 666 681, 2009. [Wang et al., 2010] Zhe Wang, Kewen Wang, Rodney Topor, and

Jeff Z. Pan. Forgetting for knowledge bases in DL-Lite. Annals of Mathematics and Artificial Intelligence, 58(1-2):117 151, 2010. [Wang et al., 2014] Yisong Wang, Yan Zhang, Yi Zhou, and

Mingyi Zhang. Knowledge Forgetting in Answer Set Programming. Journal of Artificial Intelligence Research, 50(1):31 70, 2014. [Zhang and Foo, 2006] Yan Zhang and Norman Y. Foo. Solving logic program conflict through strong and weak forgettings. Artificial Intelligence, 170(8-9):739 778, 2006. [Zhang and Zhou, 2009] Yan Zhang and Yi Zhou. Knowledge forgetting: Properties and applications. Artificial Intelligence, 173(16-17):1525 1537, 2009.