Belief Update for Proper Epistemic Knowledge Bases

1 Introduction

Reasoning about the nested beliefs of others is important in many multi-agent scenarios. Epistemic and doxastic modal logics lay a solid groundwork to approach such reasoning. Hintikka's seminal work [Hintikka, 1962] proposed a logic for knowledge at the individual level, while Fagin et al. [1995] were some of the first to look at multi-agent logics, including formal models of concepts such as common knowledge and belief. While such formalisms offer expressive logics with sound and complete proof systems, the computational complexity of these logics is high: Ladner [1977] proved that satisfiability in logic KDn for a single agent is NP-complete, while Halpern and Moses [1985] demonstrated that for multiple agents, the problem is PSPACE-complete.

Proper Epistemic Knowledge Bases 1 (PEKB) Lakemeyer and Lesp´erance [2012] are syntactic epistemic belief bases that aim to overcome this complexity. While syntactic treatments of belief and knowledge have been proposed in the past; e.g. [Eberle, 1974; Konolige, 1983], PEKBs place restrictions on the syntax of formulae to provide desirable computational properties. Lakemeyer and Lesp´erance define a PEKB as a set (or conjunction) of restricted modal literals (RML), in which RMLs are modal literals that do not contain conjunction, disjunction, >, or ?. They show how to compile a PEKB into a set of prime implicates, similar to the method employed by [Bienvenu, 2008; 2009] for the logic Kn. This allows entailment queries to be answered in polynomial time by structurally traversing the prime implicates instead of querying the original belief base. The cost is that the compilation into prime implicates is exponential. PEKBs have been shown to be expressive enough for many applications, such as collaborative filtering [Lakemeyer and Lesp´erance, 2012], epistemic planning problems such as gossip protocols [Muise et al., 2015a], and team formation [Muise et al., 2015b].

1 We will use the term belief bases to acknowledge that formulae in a PEKB can be incorrect.

Recently, Muise et al. [2015c] showed that, if a PEKB is consistent, compilation into prime implicates is not required. Thus, entailment queries can be formed directly on a consistent PEKB, avoiding the costly compilation step. However, this approach requires a PEKB to be maintained consistent if new beliefs are inserted as the world changes.

In this paper, we present an approach for updating a PEKB as new beliefs about changes in the world are added. The update operator ensures that the belief base remains consistent when new beliefs are added by first removing any formula in the belief base that contradicts the new information, called belief erasure [Katsuno and Mendelzon, 1991], and removing only this information.

Such a mechanism is not straightforward. Consider a belief base containing a single formula ⇤i⇤jp, meaning that agent i believes that agent j believes that p is true. If we erase the belief }i⇤jp from the belief base, we need to remove the formula ⇤i⇤jp, because this entails the erased belief 2 . However, if we simply remove ⇤i⇤jp, we have removed more than is required: the formula ⇤i}jp also holds in the original belief base, but is not entailed by the erased belief, so should hold in new belief base. Thus, as well as removing conflicting RMLs, a belief update mechanism should also calculate the strongest implicates that entail the old belief base but do not contradict the update formulae.

2 In any logic containing the axiom D.

We show that due to the restricted syntax of PEKBs, this update can be computed syntactically in polynomial time, despite the update process being non-trivial. We then assess the mechanism against the (KM) postulates for belief update and erasure [Katsuno and Mendelzon, 1991].

In Section 2, we present background on epistemic logic, while in Section 3, we introduce PEKBs and show some properties that enable efficient computation of entailment and belief update. In Section 4, we present operators for belief erasure and update on PEKBs, show that these can be computed in polynomial time, and assess them against the KM postulates for belief update. Section 5 concludes the paper.

2 Background and RelatedWork

In this section, we briefly present some background material on epistemic and doxastic 3 logics that is required for the paper. In particular, we are interested in the modal logic KDn, which we present here briefly (for a more complete treatment, see Fagin et al. [1995]).

Let P and Ag respectively be finite sets of propositions and agents. The set of well-formed formulae, L, for multi-agent epistemic logic is obtained from the following grammar:

in which p 2 P and i 2 Ag. Informally, ⇤iφ means that agent i believes φ. The grammar permits statements of the form ⇤i⇤j⇤kp, meaning that agent i believes that agent j believes that agent k believes that p is true. Such nestings can be arbitrarily long, and we use depth(φ) to refer to the maximum number of such nestings in the formula φ.

The semantics can be given to this language using Kripke structures [Fagin et al., 1995]. Each Kripke structure is a tuple M = (W↪ ⇡↪R1↪ ▷ ▷ ▷Rn), in which W is the set of all worlds considered in a model, ⇡ : W ! 2P is a function that maps each world to the set of propositions that hold in that world, and each Ri ✓ W ⇥W (for each i 2 Ag) is a belief accessibility relation. Each agent has an accessibility relation that captures the agent's uncertainty about the world such that for the actual world, w, the set Ri(w) is the set of worlds that agent i considers possible: Ri(w) = ¶w0 ♣ Ri(w↪w0 )♦.

Given these definitions, the satisfaction of a formula φ in a Kripke structure M and a world w is denoted as M↪ w ✏ φ, and it is defined inductively over the structure of φ:

Entailment is defined as: φ ✏ if and only if for every model M and world w such that M↪w ✏ φ, we have M↪w ✏ .

Additional operators for _, ⊃, and ⌘ can be derived in the usual way, as can > (true) and ? (false). Further, we use a second modal operator, }iφ, defined as }iφ ⌘ ≻⇤i≻φ.

3 For simplicity, we will follow convention and use "epistemic" to refer to both knowledge and belief throughout the paper.

Placing certain constraints on Kripke structures leads to specific properties of knowledge or belief, which can be represented as axioms of the logic [Fagin et al., 1995]. We are particularly interested in the systems containing the axioms K and D. The axiom K holds for any standard modal logic, while axiom D holds if the Kripke structure is serial:

Axiom D states that an agent cannot have inconsistent beliefs: if an agent believes φ, then it cannot believe ≻φ as well. In this paper we consider consistent belief bases, and so we will assume that axiom D holds. One way to achieve a consistent belief base is to use a belief update mechanism. As the world changes and new beliefs are added, any old beliefs that contradict the new beliefs are erased.

While belief update has been long studied for propositional belief bases; e.g. see the following for a selection of work that has influenced this paper: [Lang, 2007; Herzig and Rifi, 1999; Herzig et al., 2013; Katsuno and Mendelzon, 1991; Baral and Zhang, 2005], belief revision is gaining attention in epistemic logic; e.g. see [Van Ditmarsch, 2005; van Ditmarsch et al., 2007; Van Benthem, 2007], and action models provide a way to update epistemic knowledge bases given the observation of an action [van Ditmarsch et al., 2007; Baltag et al., 1998; Son et al., 2015], the concept of updating a set of nested epistemic formulae with another has received minimal study, with existing work studying the problem from a model-based perspective unsuited for tractable belief update of PEKBs [Baral and Zhang, 2005; Zhang and Zhou, 2009].

3 Proper Epistemic Knowledge Bases

Lakemeyer and Lesp´erance [2012] define a PEKB as a belief base consisting of sets (conjunctions) of restricted modal literals (RMLs). Each RML satisfies the following grammar:

Note that each RML is in negation normal form (NNF), i.e., negation appears only in front of propositional variables, and any formula comprising an arbitrary string of modal operators terminated with a literal can be converted into NNF via simple re-write rules [Lakemeyer and Lesp´erance, 2012].

We use Lit(φ) to refer to the literal at the end of RML φ; e.g. Lit(⇤i}jp) = p.

Lakemeyer and Lesp´erance show how to compile PEKBs into a prime implicate formula, and query the compiled formula, building on earlier work in more general modal logic [Bienvenu, 2008; 2009]. They show that the size of a compiled prime implicate formula is at most exponential in the depth of the PEKB φ, rather than double exponential in the general case as shown by Bienvenu, with a worst-case execution time of O(♣φ♣d+2 ), where φ is the formula representing the belief base and d is the maximum depth of a modal literal in φ. The complexity of a query of this formula is only O(n2 ), in which n is the size of the belief base. The approach proposed by Lakemeyer and Lesp´erance is sound, and is complete for formulae that are logically separable - an important concept in this paper.

Definition 1 (Logical Separability [Lakemeyer and Lesp´erance, 2012]). The set of RMLs P is logically separable if and only if for every consistent set of RMLs P 0 the following holds:

Intuitively, a set of formulae is logically separable if we cannot infer anything by combining two or more formulae from the set. For example, the formulae ¶⇤ip↪⇤i(p ⊃ q)♦ is not logically separable, because we can infer ⇤iq from the combination of the two formulae in the set. The set ¶⇤ip↪ ⇤i(p ⊃ q)♦[¶}i≻q♦ is inconsistent, but }i≻q is consistent with both other formulae individually. Logical separability plays an important role later in this paper.

In more recent work, Miller et al. [2016] extended PEKBs to handle a restricted form of disjunction: 'knowing whether' a proposition holds, without knowing that it holds or does not hold. They show that the desirable computational properties hold even with the introduction of this limited form of disjunction, although they only prove completeness for a smaller set of formulae than Lakemeyer and Lesp´erance.

In the remainder of this section, we explore some properties of PEKBs that are referred to throughout the paper.

Theorem 1. Given a PEKB P = (γ ^}i 1 ^ ▷ ▷ ▷ ^}i m^ ⇤iχ1 ^ ▷ ▷ ▷ ^⇤iχn), we have that P ♣= ? i↵ at least one of the following:

• (a) γ ♣= ?
• (c) χ1 ^ ▷ ▷ ▷ ^χn ♣= ?.
• (b) j ^χ1 ^ ▷ ▷ ▷ ^χn ♣= ? (for some j)

Proof. A proof for the logic Kn (for which only parts (a) and (b) above are required) is presented by Bienvenu [2009] (see Theorem 1, part (3)). It is straightforward to see that with the addition of the axiomD, that part (c) must be added as a consistent PEKB cannot contain the formula ⇤i?.

The following lemma is a property of the logic KDn [Lakemeyer and Lesp´erance, 2012].

Theorem2. Given a consistent PEKBP and RML , if P ♣= then 9φ 2 P, s.t. φ ♣=

Proof. This theorem was argued informally by Muise et al. [2015c], but here we prove this inductively on the structure of . Assume P = (γ^}i 1^▷ ▷ ▷^}i m^⇤iχ1^▷ ▷ ▷^⇤iχn).

The case of ⌘ }i 0 is similar. If P ♣= }i 0 , then from Theorem 1, it follows that either for some j 2 ¶ 1↪ ▷ ▷ ▷ ↪ m♦, we have that j ^ χ1 ^ ▷ ▷ ▷ ^ χn ♣= 0 , or that χ1 ^ ▷ ▷ ▷ ^ χn ♣= 0 . By induction, it must be that j ♣= 0 or χk ♣= 0 for some χk 2 ¶χ1↪ ▷ ▷ ▷ ↪ χn♦. From Lemma 1 and axiom D, we know that either }i j ♣= }i 0

The case of ⌘ γ is straightforward because PEKBs contain no disjunction. For the ⌘ ⇤i 0 case, P ♣= ⇤i 0 iff P ^}i≻ 0 ♣= ?. From Theorem 1 and the assumption that the PEKB is consistent, it follows that χ1 ^ ▷ ▷ ▷ ^ χn ♣= 0 . By induction, there must be some χk 2 ¶χ1↪ ▷ ▷ ▷ ↪ χn♦ such that χk ♣= 0 . From Lemma 1, we know that ⇤iχk ♣= ⇤i 0 and that ⇤iχk 2 P , so this case holds.

(where }i j 2 P), or ⇤iχk ♣= }i 0 (where ⇤iχk 2 P); so this case holds. From the three cases, the theorem holds.

From the above theorem, it is clear to see that if a PEKB is inconsistent, this inconsistency can be detected by checking all pairwise RMLs.

Corollary 1. A consistent PEKB is logically separable.

This follows from Definition 1 and Theorem 2.

Corollary 1 is an important property in the context of belief update: given a PEKB P , updating it with a new RML φ, we only need to check φ against each element in P to check if it is inconsistent with the belief base.

4 Belief Erasure and Update

In this section, we present a belief update mechanism for PEKBs. Given two PEKBs P and Q, P ^ Q is the PEKB resulting from an update of Q on P , defined as follows:

Thus, any resulting model P 0 (a PEKB) must entail the Q, and anything that has changed as a result of the update must be as a result of the new information Q. This definition is a re-casting of the definition of belief update based on formula/variable dependence proposed by Herzig et al. [2013], in which our models are based on PEKBs, and the definition of the dependence function is that depends on φ is φ ♣= .

in which Mod(P) is the set of models (in this case we just use PEKBs) that entail P; i.e. ¶P 0 ♣ P 0 ♣= P♦.

This section presents an algorithm for computing a unique PEKB that conforms to the definition of Mod(P ^Q), and in which the resulting PEKB is prime; that is, none of the RMLs in the updated PEKB are entailed by any other - they are all prime implicates of the PEKB.

As our update operator is defined according to the 'forgetthen-conjoin' model, we first define a belief erasure operator, and then define the belief update operator, which uses the erasure operator to 'forget'.

4.1 PEKBs as posets

For definition purposes, we consider a PEKB as a partiallyordered set (poset) (P↪ ♣=). Given a propositional literal p (or negated propositional literal) and a string s of modal operators, we can form a bounded poset from the set (S↪ ♣=), in which S is the set of RMLs ending in p (or ≻p) all of the same depth. For example, see the Hasse diagram representation in Figure 1. The poset is bounded, with the top element }}}p and the bottom element ⇤⇤⇤p.

Definition 2 (Upwards and downwards closure). Given an RML φ, we define the upward closure "φ of φ as the upward closure with respect to its poset, defined as:

We use P to denote the PEKB that contains the negation of every RML in P; that is P = ¶≻φ ♣ φ 2 P♦

The downward closure of φ, denoted #φ, is just "≻φ; that is #φ = ¶ ♣ ♣= φ♦.

The upward closure of a PEKB P is "P = Sφ2P "φ. The downward closure of a PEKB P is defined as "P .

We call a PEKB P prime if and only if all elements in P are prime implicates of P (maximal elements); that is, for all φ↪ 2 P, if φ ♣= then ♣= φ. The set of maximal elements of a PEKB is denoted max(P). Thus, for a prime PEKB P and an RML φ, we have that P ♣= φ iff φ 2 "P .

4.2 Belief Erasure

Our definition of belief update in PEKBs uses the 'forgetthen-conjoin' approach of first removing any beliefs that conflict with the update, and then adding the update. This 'forgetting' process, which Katsuno and Mendelzon [1991] term belief erasure, is not simply the act of subtracting the negation of the RMLs in the update, because we must also remove any RML that implies the negated update. For example, given the PEKB ¶⇤ip♦, removing }ip should also remove ⇤ip; otherwise, the belief base would still entail }ip.

Further, a belief erasure operator should follow the principle of minimal change: when removing belief from an existing belief base, we should remove only what we must so that the belief base no longer entails the removed belief. As an example, consider the Hasse diagram in Figure 1, representing a PEKB containing a single RML ⇤⇤⇤p. If we want to erase the RML ⇤}}p, we must remove ⇤⇤⇤p, otherwise after the erasure, ⇤⇤⇤p will remain in the PEKB, and therefore ⇤}}p would still hold. However, after the erasure, the RML }⇤⇤p should still hold: it held before the update and we have not erased it or any of its implicates. All RMLs below }⇤⇤p in the poset need not be added, because }⇤⇤p is a prime implicate of those.

Given two PEKBs P and Q, the PEKB P _ Q, the set of models resulting from erasing Q from P, is defined as fol-

Thus, any new model must entail everything previously in P , except the RMLs that are erased (P ∩ P 0 ), which must be erased as a result of Q.

Definition 3 (Belief erasure in PEKBs). Given PEKBs P and Q, we define the erasure of Q from P , denoted as P _ Q, as:

That is, take the upward closure of P and remove the downward closure of Q, removing any non-prime RMLs. This removes Q and anything that implies it, leaving those things that are in the upward closure of P but that do not entail Q.

It is straightforward to see that this corresponds with the definition of Mod(P _Q) in Equation 1, and that the resulting PEKB is prime. However, the computational complexity of calculating the closure of a PEKB is exponential in the size of the PEKB and depth of RMLs in the PEKB. We next define a method for computing this in polynomial time using syntactic transformation of the elements inside the PEKB.

From Theorem 2, we know that a PEKB is logically separable, so we can perform erasure and update by considering just the pairs of RMLs from PEKBs P and Q respectively. Thus, we first define the erasure between two RMLs.

Definition 4 (φ- ). Given two RMLs φ and , the erasure of with respect to φ, defined as φ - , is the following algorithm:

1. If φ 6♣= return ¶φ♦.
2. If = > (the top element in the poset), return ¶♦. Note that any propositional literal is the top element of its poset.
3. For each modal operator index that is ⇤i in both φ and , create a new RML that is equivalent to φ but with }i at that index. Return this set of new RMLs.

Consider the example from Figure 1, in which ⇤⇤⇤p is the element in the PEKB, and we calculate ⇤⇤⇤p-⇤}}p. It is clear that ⇤⇤⇤p ♣= ⇤}}p and that we are not erasing the top element. The first index is the only one in which both modal operators are ⇤ operators, so we create one new RML with the ⇤ replaced by }, to get the new RML }⇤⇤p.

This syntactic transformation resembles Dalal's treatment of belief revision in propositional belief bases [Dalal, 1988], although this is over the space of RMLs instead of conjunctions of propositional letters.

As a less trivial example, consider ⇤⇤⇤p - }⇤⇤p. In this case, we have two indices in which both RMLs contain a ⇤. Thus, the result is the two RMLs ⇤⇤}p and ⇤}⇤p, which is the set of maximal elements in "⇤⇤⇤p ∩ #}⇤⇤p.

Proof. Step 1: if φ 6♣= then "φ ∩ # = "φ, and the only maximal element is clearly φ.

Step 2: Step 3 determines the set of RMLs that correspond to set of prime implicates after subtracting one RML from

Algorithm 1: Belief erasure

Input: PEKBs P and Q Output: P _ Q 1 P 0 = list(P) 2 R0 = ; 3 i = 0 4 while i < ♣P 0 ♣ do 5 φ = P 0 (i) 6 for 2 Q do 7 if φ- 6= ¶φ♦ then 8 P 0 = P 0 · list(φ- ) 9 R0 = R0 [ ¶φ♦ 10 i = i +1 11 return set(P 0 ) ∩ R0 ;

another. If is the top element, then this set of RMLs corresponds to top itself, so we must remove φ entirely.

Step 3: We need to find the strongest prime implicates P 0 such that φ ♣= P 0 and P 0 6♣= . Clearly, P 0 ⇢ "φ, so all elements in P 0 must be the same as φ, but with some ⇤i operators substituted with }i operators (e.g., see Figure 1).

For an RML 0 2 P 0 that is like φ with more than one ⇤i substituted by }i, 0 cannot be prime. There must be some φ0 2 P in which exactly one of those operators is substituted, and clearly φ0 ♣= 0 . This establishes that substituting more than one ⇤i operator in φ results in a non-prime RML.

All that remains is to show that all RMLs that have one operator substituted are also prime. Consider any φ0 2 P 0 . The modal operator index where the operator was substituted is }i. For all other 0 2 P 0 , the corresponding operator is ⇤i in φ, so it must be that φ0 6♣= 0 . Thus, the theoremholds.

We abuse notation here because φ- actually returns a set of elements, but this proposition states that it does not matter in which order formulae are erased. This holds because from Theorem 3 we know that φ - is equivalent to ¶φ♦ _ ¶ ♦, and that the _ operator is just defined using set complement.

Algorithm 1 defines a function erase(P↪Q) for erasure over PEKBs. The functions list and set convert a set to a list and vice-versa. This algorithm creates a list P 0 from P, and iterates over pairs of RMLs in P 0 and Q. For each pair, the algorithm assesses if φ needs to be replaced (if φ- 6= ¶φ♦). If so, it adds φ into the set R0 , which represents the set of RMLs that will be removed, and adds φ- to the end of P 0 to be assessed against Q later (in case the new RMLs should also be erased by another element in Q). Finally, remove R0 from the set of elements in P 0 , and returns this.

Proof. This follows from Theorem 3 and Proposition 1.

The worst-case execution time of Algorithm 1 is polynomial in the size and depth of P and Q. φ- creates at most d new RMLs, where d = depth(φ) (at most one for each ⇤i operator). Thus, the algorithmwill perform ♣P♣ · d · ♣Q♣ iterations over the inner loop. The calculation of φ- is at worst linear in the depth of φ or , meaning that in the worst case, the complexity is O(♣P♣ · ♣Q♣ · 2d).

4.3 Belief Update

Given a belief erasure operator, belief update for a PEKB is straightforward: update is forget (erase) then conjoin. We use t as the conjunction operator, and this simply means to merge two PEKBs P and Q, eliminating any RML that is not prime in the set P [Q; that is, P tQ =max(P [Q).

Definition 5. Given PEKBs P and Q, we define belief update of P with Q, denoted as P ^ Q, as follows:

That is, remove anything that conflicts with Q, then add the elements in Q, and take the maximal elements from this.

It is straightforward to see that for prime PEKBs P and Q, a polynomial-time algorithm for ^ can be implemented by using the erase function defined in Algorithm 1 to erase Q, and then adding Q while removing any RML that is subsequently no longer prime.

Thus, we have defined belief erasure and belief update for PEKBs, and presented algorithms for computing these in polynomial time.

4.4 KMPostulates for Belief Update

Katsuno and Mendelzon [1991] propose a set of postulates for belief update called the Katsuno-Mendelzon (KM) postulates. These postulates, which echo the AGM postulates for belief revision [Alchourr´on et al., 1985], specify eight properties that a belief update operator should have to be an appealing update mechanism (phrased using our notation):

• U3 If P and Q are satisfiable, then P ^ Q is satisfiable

• U4 If P ⌘ P 0 and Q ⌘ Q0 then P ^Q ⌘ P 0 ^Q0
• U6 If P ^ Q ♣= R and P ^ R ♣= Q then P ^ Q ⌘ P ^ R
• U5 (P ^Q) tR ♣= P ^ (QtR)
• U7 If P is complete then (P ^Q)t(P ^R) ♣= P ^ (Q_R)

Because PEKBs do not permit disjunction, U7 and U8 are not relevant for our belief update operator.

Despite their widespread use, it is not commonly accepted that all postulates are desirable for all belief update operators. Herzig and Rifi [1999] argue that only postulates U1, U3, U8, and (possibly) U4 should be satisfied by all update operators.

Theorem 5. KM postulates U1, and U3-U6 hold for PEKB belief update operator ^. U2 holds if P is satisfiable.

For the proof of this theorem, see the extended version of this paper [Miller and Muise, 2016].

Katsuno and Mendelzon [1991] present the so-called representation theorem, which shows the completeness of the belief update operator. It is clear that the pre-order on interpretations defined by Katsuno and Mendelzon can simply be defined over the poset corresponding to the elements in the PEKB. Due to the logical separability of PEKBs, Definition 5 amounts to an equivalent notion of Katsuno and Mendelzon's representation theorem.

4.5 KMPostulates for Belief Erasure

Katsuno and Mendelzon [1991] also propose a set of postulates for belief erasure based on the principle of minimal change: when removing belief from an existing belief base, we should remove only what we must so that the belief base no longer entails the removed belief. These postulates phrased using our notation are:

• E2 If P ♣= Q then P _Q ⌘ P

• E3 If P is satisfiable then P _ Q 6♣= Q
• E5 (P _Q) tQ ♣= P

E8 does not make sense because PEKBs cannot contain disjunctive formulae.

Katsuno and Mendelzon define an identity, a mirror of the identity Harper introduced that expresses belief contraction in terms of set operations and belief contraction [Harper, 1976]. Katsuno and Mendelzon's identity can be expressed as:

in which P uQ = max("P \ "Q). Intuitively, this identity stipulates that erasing Q should be the same as restricting the belief base to what would hold if the negation of Q was added.

Katsuno and Mendelzon show that if the identity in Equation 2 holds and the ^ operator satisfies postulates U1-U4 and U8, then the _ operator satisfies postulates E1-E5 and E8. The following counterexample demonstrates that Equation 2 does not hold on our operators: P = ¶⇤ip♦ and Q = ¶}ip↪ }i≻p♦. From this, P _ Q = ¶♦, while P ^ Q = ¶}ip↪ }i≻p♦, which when intersected with "P leaves ¶}ip♦.

This mirrors the Levi identity for belief revision and contraction [Levi, 1978]. They show that if this identify holds and the _ operator satisfies E1-E4 and E8, then ^ satisfies U1U4 and U8. Equation 3 is just our definition of belief update, and Katsuno and Mendelzon's theorem about the relationship between the two sets of postulates holds:

Theorem 6. KM postulates E1, E3, and E4 hold for the PEKB belief erasure operator. E2 holds if P is satisfiable.

For the proof of this theorem, See the extended version of this paper [Miller and Muise, 2016].

The E5 postulate does not hold. As a simple counterexample to this, consider the PEKBs P = ¶⇤ip♦ and Q = ¶}ip♦. Erasing Q from P will result in an empty set, and then adding Q will result in ¶}ip♦, which does not entail ⇤ip.

Finally, we note briefly on a controversial 4 postulate - the recovery postulate:

4 See a discussion of the issues surround the postulate in [Makinson, 1987].

This extends postulate E5, using ^ instead of t. The counterexample for E5 serves to show this postulate does not hold. However, we can characterise precisely when postulate E5 and the recovery postulate are satisfied: when Q = #Q. This follows directly from the definition of _.

4.6 Relationship to belief revision and contraction

It is noted earlier that because PEKBs do not permit disjunction, postulates U7, U8, and E8 are not relevant for our belief update and erasure operators. This is important because postulates U7, U8, and E8 distinguish belief update from belief revision [Katsuno and Mendelzon, 1991].

In the case of PEKBs, belief update and belief revision essentially collapse to the same operator. Our belief update operator satisfies the postulates for belief revision (postulates R1-R5) proposed by Alchourr´on et al. [1985], which are equivalent to postulates U1-U5, except that postulate U2 is weaker than R2:

Postulate R2 holds for our update operator: P ^Q is equivalent to (P _ Q) t Q. If P t Q is satisfiable, then there cannot be any RML φ entailed by both P and Q. Therefore, P _Q ⌘ P, and thus P ^Q ⌘ P _QtQ ⌘ P tQ.

However, the corresponding relationship does not hold for belief contraction and erasure. Postulates C1-C5 for belief contraction [Alchourr´on et al., 1985] echo those of E1-E5 of belief erasure, except with the addition of E8 for erasure, and that the postulate E2 is weaker than its counterpart, C2:

This is trivially false. Consider the PEKBs P = ¶p↪ q♦ and Q = ¶q↪ r♦. It is clear that P 6♣= Q, but that P _ Q = ¶p♦. Thus, our belief update operator satisfies the postulates proposed by Alchourr´on et al. [1985] for a belief revision operator, but our belief erasure operator does not satisfy the postulates for a belief contraction operator.

5 Conclusion

In this paper, we present belief update and erasure operators for PEKBs. Our update operator is based on the 'forget-thenjoin' theory, meaning that everything that conflicts with the update is removed before the updated beliefs are added. The result is a consistent belief base that entails the new beliefs and any prior beliefs that do not conflict with the new beliefs. We present algorithms for computing belief erasure and update in polynomial time, and then show that our mechanism is sound with respect to the KM postulates and complete.

Acknowledgements This research is funded by Australian Research Council Discovery Grant DP130102825, Foundations of Human-Agent Collaboration: Situation-Relevant Information Sharing.