# knowing_whether_in_proper_epistemic_knowledge_bases__f544c599.pdf

Knowing Whether in Proper Epistemic Knowledge Bases

Tim Miller, Paolo Felli, Christian Muise, Adrian R. Pearce, Liz Sonenberg Department of Computing and Information Systems, University of Melbourne {tmiller,paolo.felli,christian.muise,adrianrp,l.sonenberg}@unimelb.edu.au

Proper epistemic knowledge bases (PEKBs) are syntactic knowledge bases that use multi-agent epistemic logic to represent nested multi-agent knowledge and belief. PEKBs have certain syntactic restrictions that lead to desirable computational properties; primarily, a PEKB is a conjunction of modal literals, and therefore contains no disjunction. Sound entailment can be checked in polynomial time, and is complete for a large set of arbitrary formulae in logics Kn and KDn. In this paper, we extend PEKBs to deal with a restricted form of disjunction: knowing whether . An agent i knows whether ϕ iff agent i knows ϕ or knows ϕ; that is, iϕ i ϕ. In our experience, the ability to represent that an agent knows whether something holds is useful in many multi-agent domains. We represent knowing whether with a modal operator, Δi, and present sound polynomial-time entailment algorithms on PEKBs with Δi in Kn and KDn, but which are complete for a smaller class of queries than standard PEKBs.

Introduction

Reasoning about the nested beliefs or knowledge of other agents is essential for many collaborative and competitive tasks. While highly expressive doxastic and epistemic logics exist for this (Fagin et al. 1995), such logics are computationally expensive. To implement agents that can efficiently reason about other agents in complex scenarios, approximations of these logics are necessary in many cases. Proper epistemic knowledge bases (PEKBs), proposed by Lakemeyer and Lesp erance (2012), are one such approximation. PEKBs are syntactic knowledge bases that contain sets of restricted modal literals (RMLs), which are modal literals that contain no conjunction or disjunction. Lakemeyer and Lesp erance (2012) show that, for the epistemic logic Kn, a PEKB can be compiled in exponential time into a special normal form, called prime implicate normal form (PINF), which is logically equivalent to the original PEKB, and database-like entailment queries can be made on these compiled form formulae in polynomial time. Muise et al. (2015b) extended this work to show that, if the knowledge base is known to be consistent, for example due to the use of a sound belief update operator, then entailment queries

Copyright c 2016, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

can be done in polynomial time without the expensive precompilation step. In both cases, entailment queries are complete for a reasonably large set of arbitrary modal logic formula, and sound for any query. Muise et al. (2015a) used this to compile a multi-agent epistemic planning problem into a classical planning problem, allowing plan and policy generation over multi-agent epistemic states. The lack of disjunction is a restriction that is acceptable for some scenarios, but clearly not all; however extending PEKBs to include disjunction would eliminate the desirable computational properties. We believe the next best opportunity is to include a restricted form of disjunction: knowing whether . An agent knows whether ϕ is true or in the case of belief logics, is opinionated as to whether ϕ is true if they know ϕ or they know ϕ. Formally, iϕ i ϕ. The ability to model knowing whether is useful in many domains, such as for action preconditions in planning (Scherl and Levesque 1993), diagnostic planning applications (Baier, Mombourquette, and Mc Ilraith 2014), and in scenarios such as gossip (van Ditmarsch and Kooi 2015), muddy children (Fagin et al. 1995), and questioning (Aloni, Egr e, and De Jager 2013). In particular, knowing whether is useful in multi-agent domains in which agents know (or observe) that events occur without observing the outcome of the event itself. Consider the following scenario involving multi-vehicle search and rescue. If one unmanned vehicle (vehicle 1) has surveyed a sequence of points looking for survivors, we know that the vehicle knows whether there are survivors at surveyed points. If another vehicle (vehicle 2) observes a survivor at point A in the sequence, it can then infer that the first vehicle knows that there is a survivor (( 1survivor 1 survivor) 2survivor 1survivor) and may assume that vehicle 1 has returned to base to report without finishing its survey, as pre-scripted. Vehicle 2 can now re-plan that: (a) it should survey the remaining points; and (b) it need not enact a rescue plan. Without being able to represent that vehicle 1 knows whether there is a survivor at point A, vehicle 2 cannot infer this without regressing into the past , because it does not have 1survivor 1 survivor in its knowledge base, so cannot infer that 1survivor. In our experience modelling real applications, the lack of disjunction in knowledge bases has only been problematic for these knowing whether cases. In this paper, we extend PEKBs to include knowing

Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence (AAAI-16)

whether. Rather than model this as an explicit, yet restricted disjunction, we follow Fan et al. (2015) by modelling knowing whether as its own modal operator, Δi, defined as Δiφ iφ i φ. After providing the necessary background for the paper in the following section, we show how to compile an extended PEKB into a prime implicate normal form in exponential time and space, and how to perform entailment queries for logic Kn in polynomial time, preserving the nice computational properties from Lakemeyer and Lesp erance (2012). The cost is a less expressive set of complete queries. We then show that, as with Muise et al. (2015b), a consistent knowledge base in logic KDn can be queried (for a smaller class of queries) in polynomial time without any prior compilation. We conclude with a discussion and future work. The end result is a model for efficiently reasoning about nested beliefs in multi-agent environments that would be suitable for many scenarios.

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

ϕ ::= p | ϕ ϕ | ϕ | iϕ

in which p P and i Ag. Informally, iϕ means that agent i knows (or believes1) ϕ. The shorthand iϕ is the dual of iϕ, defined as iϕ i ϕ. Operators for , , and can be derived in the usual way. The semantics of this logic are given using Kripke structures. A Kripke structure is a tuple M = (W, π, R1, . . . , Rn), in which W is the set of all possible worlds, π W 2P is a function that maps each world w to the set of all propositions that hold in w, and Ri W W (for each i Ag) is an accessibility relation which captures each agent s uncertainty about the world see (Fagin et al. 1995) for details. The formula iϕ holds in w iff ϕ is true in all worlds that the agent i considers possible at w, while iϕ means that the agent considers ϕ possible, thus holding in at least one possible world. The satisfaction of a formula ϕ in a structure M and a world w, denoted as M, w ϕ, is defined inductively over the structure of ϕ: M, w p iff p π(w) M, w ϕ ψ iff M, w ϕ and M, w ψ M, w ϕ iff M, w ϕ M, w iϕ iff for all v Ri(w), M, v ϕ

We say that ϕ entails ψ, written ϕ |= ψ iff for every model M and world w such that M, w ϕ, we have M, w ψ. Kripke structures with specific constraints lead to specific properties (or axioms) of knowledge or belief (Fagin et al. 1995). For example, axiom K holds for any Kripke frame, while the axiom D holds on serial Kripke frames, resulting in the axioms: K i(ϕ ψ) ( iϕ iψ) (Distribution) D iϕ i ϕ (Consistency)

1For the remainder of the paper, we will use the term knowledge to mean both knowledge and belief.

Combinations of axioms result in different logics. Here, we consider logics Kn (axiom K only) and KDn (K and D), in which n specifies that there are multiple agents in the model. Example 1. Consider an example, taken from Muise et al. (2015b) about two agents, Bob and Alice, who are coworkers. Bob knows Alice has applied for a promotion. Bob sees an envelope containing the outcome of the promotion, but has no information about whether Alice has opened the envelope. However, Bob knows that if Alice has opened the envelope, then Alice will know whether she has gained her promotion, and that if Alice has not opened the letter, she will not know whether she has gained her promotion. Assuming that opened and promoted represent that Alice has opened the letter and has been promoted respectively, we can represent the above using modal logic as follows:

B(opened ( Apromoted A promoted)) B( opened ( Apromoted A promoted))

Such logics are expressive, but computationally present several challenges. In the single agent case, Ladner (1977) showed that satisfiability is NP-complete, while Halpern and Moses (1985) demonstrated satisfiability is PSPACEcomplete for multiple agents, but only NP-complete if the nesting of modal formulae is bounded (Halpern 1995). As such, syntactic approaches to knowledge bases have been investigated, with Eberle (1974) one of the first to consider syntactic knowledge bases, and Konolige (1983) the first to consider syntactic belief bases with nested belief.

Knowledge compilation and prime implicates Prime implicates have been used to mitigate the complexity of checking satisfiability and entailment in syntactic knowledge bases. A formula ϕ is a prime implicate of a knowledge base KB iff KB |= ϕ (it is an implicate) and for all ϕ such that KB |= ϕ , ϕ |= ϕ implies ϕ |= ϕ (it is prime). The challenge is to calculate exactly the set of prime implicates of a knowledge base, and check entailment of a formula against the prime implicates instead of the original knowledge base. Bienvenu (2008; 2009) presents an algorithm that takes a logic Kn knowledge base and compiles it into prime implicate normal form (PINF), which is a DNFlike normal form in which all clauses are prime implicates. Essentially, a formula in PINF contains exactly the formulae required to check entailment of another formula, and nothing more. Entailment of a formula on the PINF formula can be checked in polynomial time, but the cost of generating the PINF is double-exponential in time and space.

Proper epistemic knowledge bases Lakemeyer and Lesp erance (2012) define a proper epistemic knowledge base (PEKB) as a set of restricted formulae, called restricted modal literals (RMLs), of the form:

α ::= p | p | iα | iα

Thus, a PEKB contains no disjunctive formulae. Note that RMLs are in negation normal form (NNF), i.e. negation appears only in front of propositional variables. Any Kn modal

literal can be re-written into NNF using iϕ i ϕ, iϕ i ϕ, and p p. Following Bienvenu, Lakemeyer and Lesp erance (2012) show how to compile a PEKB into PINF formula in singleexponential time and space, and how to check entailment of this PINF in polynomial time. Thus, by sacrificing expressiveness, some computational cost can be reduced. Their entailment algorithm is sound for arbitrary Kn queries, and complete for PINF formulae and for formulae in a specific normal form NF, in which the semantic relationship between formulae is restricted to a certain class. Muise et al. (2015b) showed that if a PEKB is consistent, then for a smaller class of queries, compilation to PINF is not required: the PEKB can be queried directly in polynomial time. Thus, if one uses a sound belief update mechanism on a PEKB, then the expensive compilation to PINF can be avoided.

Knowing whether in epistemic logics Fan et al. (2015) define knowing whether ϕ such that M, w |= Δiϕ iff:

for all v1, v2 Ri(w) M, v1 ϕ M, v2 ϕ

That is, at a world w, agent i knows whether ϕ if and only if all reachable worlds agree on the truth of ϕ. They also define an operator iϕ as a shorthand for Δiϕ. Note that this is not a dual operator, but a negation operator, read as: i does not know whether ϕ. They show that knowing whether is in fact equivalent to contingency logic (Humberstone 1995; Kuhn 1995) and the negation of ignorance in ignorance logic (van der Hoek and Lomuscio 2003; Van Der Hoek and Lomuscio 2004). The following properties hold for Δi: Δiϕ Δi ϕ iϕ iϕ i ϕ iϕ Δiϕ iϕ Δiϕ iϕ (with axiom D) PEKBs are not able to express the notion of knowing whether, due to the fact that it discusses uncertainty via disjunction: Δiϕ ( iϕ i ϕ). As such, a class of problems that require knowing whether are out of scope. In the remainder of this paper, we extend the notion of PEKBs to include the modal operators Δi and i into PEKBs for logics Kn and KDn, without sacrificing the desirable computational properties of PEKBs.

Extending PEKBs with Knowing whether Rather than deal with knowing whether as the disjunction of iϕ i ϕ, we use the Δi and i operators, in which Δiϕ specifies that agent i knows whether ϕ holds, and iϕ is defined as Δiϕ; that is, agent i does not know whether ϕ holds. First, we extend a definition of RMLs to include the Δi operator:

α ::= p | p | iα | iα | Δiβ β ::= p | iβ | iβ | Δiβ

Thus, the modal literals are in NNF, which includes the restriction that a negation never occurs after a Δi. As with RMLs, any modal literal, including those with Δi operators, can be written into NNF, and i can be removed completely:

Δiϕ iϕ Δi ϕ Δiϕ i ϕ iϕ iϕ iϕ i ϕ

φ1 φ2 ... φ1 φ2

φ1 φ2 ... φ1 φ2

φ1 φ2 ... φ1 φ2

φ1 φ2 . . . φ1 φ2

Figure 1: Set of models corresponding to the four Δcombinations reachable from world w for Δiφ1, Δiφ2.

In the remainder of this paper, we will use the symbol P for PEKBs. Also, to simplify the notation, we will consider a conjunction of Kn formulae γ Δiφ1 . . . Δiφl iψ1 . . . iψm iχ1 . . . iχn, in which γ is a propositional formula, φ1, ..., φl, ψ1, ..., ψm, χ1, ..., χn are formulae in Kn (KDn), so that each symbol can be used to disambiguate the outermost operator of each formula. We use α to represent RMLs, and ϕ and ψ as general Kn (KDn) formulae. We use ϕ ϕ to access conjuncts of ϕ, when ϕ is a conjunction of formulae. The introduction of Δi formulae introduces a restricted form of disjunction. For example, given the set of formulae {Δiφ1, Δiφ2}, at least four models satisfy this: one for each combinations of [ ]φ1 [ ]φ2 holding in all possible worlds. This is shown in Figure 1. Note that for each model, exactly one combination of [ ]φ1 [ ]φ2 holds at all possible worlds at w. We will refer to such combinations as Δi-combinations. The set of all Δi-combinations for agent i in PEKB P is defined formally as:

Δi-combs(P) = {

Δiψ (P\P ) ψ | P P}

Theorem 1. Given a PEKB ϕ = γ Δiφ1 . . . Δiφl iψ1 . . . iψm iχ1 . . . iχn, we have that ϕ |= iffat least one of the following:

(a) γ |= ; (b) ψj χ1 . . . χn |= (for some j); or (c) for all Δi-combinations φ of ϕ, for some j, φ ψj |=

The final point means all Δi-combinations conflict with at least one ψj.

Proof. For the right-to-left case, assume that the left side is false, and the formula is instead satisfiable. Then there must be some M, w such that M, w |= γ Δiφ1 . . . Δiφl iψ1 . . . iψm iχ1 . . . iχn. From this, M, w |= γ holds trivially, therefore γ is satisfiable. If M, w |= iψ1 . . . iψm iχ1 . . . iχn, then there exists a world w reachable from w such that M, w |= ψj χ1 . . . χn for all j, therefore, it must be that ψj χ1 . . . χn is satisfiable, for all j. For part (c), consider some Δiφu. If M, w |= Δiφu, then M, w |= iφu or M, w |= i φu. If there are several Δi formulae, M, w |= Δiφ1 . . . Δiφl iψ1 . . . iψm, it must be that for some Δi-combination φ, we have that M, w |= iφ. Therefore, for all j, there exists a world w such that M, w |= φ ψj, i.e. φ ψj is satisfiable. For the left-to-right case, suppose that the right side is false. Construct a Kripke structure and a set of worlds such that M, w |= γ, and M, wj |= ψj χ1 . . . χn for all

j, and where all wj are reachable from w. It is clear that M, w |= γ iψ1 . . . iψm iχ1 . . . iχn. Further, we know that for some Δi-combination φ, we have φ ψj is satisfiable for all j. Take this φ and add it to each reachable world w . φ is equivalent to some Δi-combination of P. Therefore, for each φu, we have that M, wj |= φu for all wj or M, wj |= φu for all wj, and therefore, M, w |= Δiφ1 . . . Δiφl. Combining with the above, M, w |= γ Δiφ1 . . . Δiφl iψ1 . . . iψm iχ1 . . . iχn, so the formula is satisfiable.

This theorem provides us with a way to determine satisfiability of Kn PEKBs, but also with a starting point for pre-compiling PEKBs into prime implicate normal form. For the remainder of the paper, we use Δi-combs (P) to denote the Δi-combinations of all subsets of PEKB P, defined as:

Δi-combs (P) =

P P Δi-combs(P ) \ { ψ | Δiψ P}

A formula φ Δi-combs (P) is thus a conjunction of positive and negated elements in Δi formulae. E.g., if P = {Δiφ1, Δiφ2}, then Δi-combs (P) = {φ1, φ2, φ1 φ2, φ1 φ2, φ1 φ2, φ1 φ2}. Note that φ1, φ2 / Δi-combs (P) as Δiφ1 Δi φ1.

Definition 1 (Prime implicate normal form (PINF)). A set of formulae Σ, is in prime implicate normal form (PINF) iff every formula in Σ is a prime implicate of Σ (as defined in the background section), and every formula is a term, where a term is defined by:

T ::= p | p | i T | i T | Δi T | T T

Note that this definition is different from Bienvenu (2009) (subsequently adopted by Lakemeyer and Lesp erance (2012)) as it pertains only to terms, not arbitrary Kn formula.

For example, the set of formulae { i j(p q), Δi jp} is not in PINF because for any model in which i jp holds, it must be that Δi jp also holds. Next, we introduce a function PEKB2PINF that converts PEKBs into a PINF formula such that the PINF formula is logically equivalent to the original PEKB, but contains only the prime implicates of PEKB. Step 1 first determines potential prime implicates that result from combining multiple RMLs. Steps 2 4 then eliminate non-prime implicates, such as the example above. Finally, step 5 determines if there are contradictions in the PEKB.

Definition 2 (PEKB2PINF(P)). The function PEKB2PINF takes a conjunction of terms2 P, and returns a PINF formula Σ. First, we define the following:

Bi(P) = {ϕ | iϕ P} Di(P) = {ϕ | iϕ P} Wi(P) = {ϕ | Δiϕ P} Prop(P) = {l | l is a non-modal literal l P}

2Note that a PEKB is just a restricted form of this where the terms are all restricted modal literals.

The PEKB2PINF algorithm is then defined as follows:

1. Let Fi(P) =

ϕ Bi(P) ϕ. Let Γ(P) = Prop(P) { i(ϕ Fi(P)) | ϕ Di(P) Bi(P) = } { i(ϕ) | ϕ Di(P) Bi(P) = } { i(Fi(P)) | Bi(P) = } {Δi(Ψ) | Ψ Δi-combs (Wi(P))}. 2. For each M(ϕ) Γ(P), where M is either i or i, replace it by M(PEKB2PINF(ϕ)). 3. For all iϕ1, Δiϕ2 Γ(P), if ϕ1 |= ϕ2, remove Δiϕ2 from Γ(P), and replace every iχ Γ(P) with i(χ ϕ2). 4. For all iϕ1, Δiϕ2 Γ(P), if ϕ1 |= ϕ2, remove Δiϕ2. 5. If any of the following hold, return : (a) i is in Γ(P) (b) both p and p are in Γ(P), (c) if Δiϕ1, iϕ2, and iϕ3 are in Γ(P) and ϕ1 ϕ2 |= and ϕ1 ϕ3 |= . Otherwise return Σ =

Note that each PINF formula will contain at most one iχ for each i: the prime implicate formed from all i formulae. This definition of PEKB2PINF is similar to Lakemeyer and Lesp erance s algorithm, except that it handles Δi formulae. The prime implicates of Δi formulae deserve discussion. Given Δiφu and Δiφv, six prime implicates result: Δiφu, Δiφv, Δi(φu φv), Δi(φu φv), Δi( φu φv), and Δi( φu φv). That is, all conjunctions of [ ]φu and [ ]φv are known whether , and all are prime implicates. While Δiφu, Δiφv |= Δi([ ]φu [ ]φv), the reverse does not hold. Consider if agent i knows whether φu and knows whether φv, then clearly agent i knows whether φu φv. However, if agent i knows whether φu φv because it knows that (φu φv), this does not imply that it knows whether φu (nor φv), because it may only know that their conjunction is false without knowing their individual truth values.

Lemma 1. Given a PINF formula Σ such that Σ P for a given PEKB P, then Δi(φu φv) Σ iff both Δiφu and Δiφv are in Σ (for φu φv).

Proof. As discussed above, Δi(φu φv) |= Δiφu (nor φv). However, Δi(φu φv) is a prime implicate of P iff both Δiφu and Δiφv are in P, because conjunction is not allowed in any Δiφj P, and Δiφu Δiφv |= Δi(φu φv).

Lemma 2. Given a PINF formula Σ = γ Δiφ1 . . . Δiφl iψ1 . . . iψm iχ such that Σ P for some PEKB P, and a formula ϵ in NNF:

(a) Σ |= l iff l γ (l is a non-modal literal) (b) Σ |= Δiϵ iff ΔiΣ Σ s.t. Σ ϵ or Σ |= iϵ i ϵ; (c) Σ |= iϵ iff iΣ Σ s.t. iΣ |= iϵ; (d) Σ |= iϵ iff χ |= ϵ

Proof. The case in which Σ |= is trivial, and we omit it. Consider (a). By Theorem 1, Σ l |= iff γ |= l. Consider (b). Σ |= Δiϵ is equivalent to Σ iϵ i ϵ |= and, by Theorem 1, either: (i) χ |= ϵ or χ |= ϵ; or (ii) φ |= ϵ or φ |= ϵ for all Δi-combinations φ. If (i) holds then Σ |= iϵ or Σ |= i ϵ, and therefore Σ |= iϵ i ϵ. If (ii) holds then since any Δiφu Σ either occurs in original PEKB, or is a combination in Δi-combs (P) of the original PEKB (or both), then by Lemma 1, we know that every such Δiφu must be in Σ. So there is some ΔiΣ Σ such that Σ ϵ. Note that the case where ϵ is of the form ϵ1 ϵ2 is not considered because Δiϵ is in NNF, and Δi(ϵ1 ϵ2) Δi (ϵ1 ϵ2) Δi( ϵ1 ϵ2). Consider (c). If Σ |= iϵ then Σ i ϵ |= , and from Theorem 1, there must be a ψj such that ψj χ |= ϵ and therefore, i(ψj χ) |= iϵ. Because Σ is in PINF, then either i(ψj χ) Σ or for some other iΣ Σ, and iΣ |= i(ψj χ). Therefore, iΣ |= iϵ. Consider (d). By Theorem 1, Σ |= iϵ iff Σ i ϵ |= iff either: (i) χ |= ϵ; or (ii) for all φ, either there exists a ψj such that φ ψj is unsatisfiable or φ ϵ is unsatisfiable. Now consider any model M, w such that, M, w |= iφ iψ1 . . . iψm. It must be that M, w |= iϵ, because there is no ψj such that φ ψj is unsatisfiable. Similarly, for any model M, w such that M, w |= i φ iψ1 . . . iψm, it must be that M, w |= iϵ for the same reason. Therefore, Σ |= iϵ. However, if Σ |= iϵ, and Σ is in PINF, then it must be that iχ |= iϵ, and thus χ |= ϵ, which is the same as (i).

Theorem 2. PEKB2PINF returns a PINF formula that is equivalent to the original PEKB P; that is Γ(P) P and every formula in Γ(P) is a prime implicate.

Proof. The proof is an extension of the proof for Lemma 2. We show the least straightforward case: Δiϵ. If Δiϵ is a prime implicate of a PEKB P, then P |= Δiϵ. As argued in the proof of Lemma 2, this means that either: (i) P |= iϵ i ϵ; or (ii) there is some combination φ Δi-combs (P) such that Δiφ Δiϵ. Because Δiϵ is a prime implicate, (ii) means that Δiφ should be in Γ(P) for all φ Δi-combs (P), which is the case. However, for case (i), if either iϵ or i ϵ holds, then Δiϵ cannot be a prime implicate, because iϵ |= Δiϵ and i ϵ |= Δiϵ. Thus, if iϕ1, Δiϕ2 Γ(P) and ϕ1 |= ϕ2, then Δiϕ2 should be excluded from Γ(P), which occurs in step 4 of PEKB2PINF.

Theorem 3. The space and time complexity of PEKB2PINF is exponential in size and depth of P.

Proof. Checking entailment between two RMLs (steps 3 and 4) can be done in linear time in the depth of the shortest RML. The algorithm from Lakemeyer and Lesp erance (2012) has worst-case time complexity of O(|P|d+2), with d being the modal depth of ϕ (accounting for the recursive calls in step 2). Our algorithm must also derive 2n Δ formulae in each recursive call, in which n is the number of Δ formula in P. Therefore, the worst-case complexity is

O(|P|d+2+|P|). The proof of the space bound follows in a similar manner.

Query evaluation In this section, we consider a querying mechanism, V , that takes a PINF formula Σ, and query ϕ in NNF, and returns 1 or 0, in which 1 is interpreted as true and 0 as unknown. This query mechanism is exactly as Lakemeyer and Lesp erance (2012), except that we need to define V for Δiϕ. Definition 3 (V [Σ, ϕ]). V [Σ, ϕ] = 1 if Σ = , otherwise:

V [Σ, ] = 1 and V [Σ, ] = 0

V [Σ, l] = 1 if l Σ, 0 otherwise

V [Σ, iϕ] = 1 for some iΣ Σ, V [Σ , ϕ] = 1 0 otherwise

V [Σ, iϕ] = 1 for some iΣ Σ, V [Σ , ϕ] = 1 0 otherwise

V [Σ, Δiϕ] =

1 if V [Σ, iϕ i ϕ] = 1 or if Δiϕ Σ 0 otherwise

V [Σ, ϕ ψ] = max(V [Σ, ϕ], V [Σ, ψ])

V [Σ, ϕ ψ] = min(V [Σ, ϕ], V [Σ, ψ])

Thus, V is a simple database query on the PINF formula for a knowledge base using a structural subsumption similar to that of Bienvenu (2009), Lakemeyer and Lesp erance (2012) and Muise et al. (2015b). Theorem 4 (Soundess of V ). Let Σ be a PEKB in PINF, and ϕ a formula in NNF. If V [Σ, ϕ] = 1 then Σ |= ϕ.

Proof. Soundness follows directly from Lemma 2, except for the first three cases, and the conjunction and disjunction cases, which all hold trivially.

Comment. To obtain a sound query mechanism, we do not actually need to consider all φ Δi-combs (P). PEKB2PINF could simply keep only those Δiα formulae from the original PEKB, and re-write queries of the form Δi(φu φv) to Δiφu Δiφv. It is easy to show that this mechanism would be sound, but that the formula produced by PEKB2PINF would not be in PINF, because Δi(φu φv) is a prime implicate. However, the complexity of this compilation approach would be O(|P|d+2) instead of O(|P|d+2+|P |). While V is sound, it is quite clearly incomplete. For example, consider the simple query (p p q) q, which is a tautology, but for which V [Σ, ϕ] = 0. Definition 4 (Query normal form). We define a normal form for queries, called query normal form (QNF):

T ::= p | p | i T | i T | Δi T | T T C ::= T | C C

A query is therefore a disjunction of terms. A formula in QNF is clearly in DNF (and therefore NNF).

Definition 5 (Logical Separability). From Lakemeyer and Lesp erance (2012): the set of formulae P is logically separable iff for every consistent set of formulae P this holds:

if P P |= then ϕ P, s.t. P {ϕ} |=

Logical separability captures the property that there are no logical puzzles hidden within P. For example, the set { ip, i(p q)} is not logically separable, because we can infer iq from the combination of the two, yet the formula i q is consistent with each individual formula.

Theorem 5 (Completeness of V for QNF queries.). Let Σ be a PEKB in PINF and ϕ a logically-separable formula in QNF. Then V [Σ, ϕ] = 1 iff Σ |= ϕ.

Proof. The left-to-right direction follows from Theorem 4. For the other direction, if Σ , the proof is immediate. If Σ , we prove by induction on the length of ϕ. The cases for propositions, iϕ, iϕ, and ϕ ψ hold from Lakemeyer and Lesp erance (2012) (Theorem 6). The ϕ ψ follows the same argument. Assume that the theorem holds for formula of length n, and that ϕ is of length n+1. If Σ |= ϕ ψ, then Σ { ϕ, ψ} is inconsistent. Because the query is logically separable, then Σ { ϕ} or Σ { ψ} is inconsistent. Thus Σ |= ϕ or Σ |= ψ, and inductively, V [Σ, ϕ ψ]. The Δiϕ case holds from Lemma 2.

Consistent knowledge bases

In this section, we consider a natural extension for KDn, namely the case when a KDn knowledge base is consistent; for example, a sound belief update mechanism is used to add new formulae to the PEKB. Working with consistent PEKBs, we can define a polynomial entailment mechanism that is complete for a restricted set of QNF formulae, and sound, but which can be performed on uncompiled PEKBs, thereby avoiding the exponential compilation step similar to PEKB2PINF. This is because we can re-write non-separable queries such as Δiϕ, iϕ |=KDn iϕ as Δiϕ, iϕ |=KDn Δiϕ iϕ, which is separable. For the remainder of this section, we use |= to mean |=KDn.

Lemma 3. Given a PEKB P = γ Δiφ1 . . . Δiφl iψ1 . . . iψm iχ1 . . . iχn and an RML α, then the following hold in logic KDn:

(a) P |= l iff l γ (l is a non-modal literal) (b) P |= Δiα iff Δiα P or iα P s.t. α |= α or α |= α (c) P |= iα iff iα P s.t. α |= α or iα P s.t. α |= α (d) P |= iα iff P |= Δiα iα

Proof. Case (a) is straightforward. For (b), P |= Δiα iff P iα i α |= , and by Theorem 1, either: χ1 . . . χn |= α or χ1 . . . χn |= α; or (ii): φ |= α or φ |= α for all Δi-combinations φ. If (i) holds, then P |= iα iα. If (ii) holds, then we know there is some φ such that φ α. Because α is an RML, then φ must also be an RML, and therefore Δiφ P.

For case (c), if P i α |= then by Theorem 13, there is a ψv such that ψv χ1 . . . χn |= α. Because P contains only RMLs, it cannot be that i(ψv χu) P for any ψv χu. Further, because α is an RML, it must be that ψv |= α or χu |= α for some u, and therefore iψv |= iα or iχu |= iα. Case (d) holds trivially from the equivalence iϕ Δiϕ iϕ in logic KDn.

Definition 6 (Reduced Query Normal Form). We define reduced query normal form (reduced QNF) as:

T ::= p | p | i T | i T | Δi T C ::= T | C C | C C

Reduced QNF formulae are therefore Boolean combinations of RMLs. They differ from QNF formulae because conjunctions are not permitted inside modal operators.

Definition 7 (U [P, ϕ]). Given a PEKB, P, and a query ϕ in reduced QNF, the query mechanism U [P, ϕ] returns 1 for true and 0 for unknown: U [P, ] = 1, U [P, ] = 0, or: U [P, l] = 1 if l P, 0 otherwise

U [P, iα] =

1 if U [Bi(P), α] = 1 or for some iα P, U [{α }, α] = 1 0 otherwise

U [P, Δiα] =

1 if U [Bi(P), α α] = 1 or if Δiα P 0 otherwise U [P, iα] = U [P, Δiα iα]

U [P, ϕ ψ] = min(U [P, ϕ], U [P, ψ])

U [P, ϕ ψ] = max(U [P, ϕ], U [P, ψ])

Theorem 6. Given a PEKB P and a query ϕ in reduced QNF, the worst-case complexity of U [P, ϕ] is polynomial on the size of P.

Proof. The worst-case complexity is O(|P| d), in which d is the depth of the knowledge base. In the worst case, for each sub-formula in ϕ, U [P, ϕ] would be required to iterate over each RML in P, recursively calling U up to d times.

Theorem 7 (Soundness and completeness of U [P, ϕ]). Let P be a set of RMLs and ϕ a logically-separable reduced QNF formula. Then U [P, ϕ] = 1 iff P |=KDn ϕ.

Proof. This follows immediately from Lemma 3, except the for simple and cases, which are trivial, and the conjunction and disjunction cases, which can be proved in the same way as the proof for soundness of V (Theorem 4).

Proposition 1. For an arbitrary KDn formula ϕ, there is an equivalent formula ϕ in reduced QNF (and therefore in QNF) that is at worst exponentially larger than ϕ, and that for a given PEKB P, P |= ϕ iff P |= ϕ .

3In fact, the case for KDn is slightly different, but does not affect the proof for consistent knowledge bases.

For PEKBs, the three modal operators distribute over conjunction and disjunction (e.g. i(ϕ ψ) iϕ iψ and P |= Δi(ϕ ψ) iff P |= Δiϕ Δiψ, in which P is a PEKB), and the resulting formula is at worst linear in the size of the original formula. The only exception is the rule rule P |= i(ϕ ψ) iff P |= ( iϕ iψ) ( iϕ iϕ), which produces a formula that is at worst 2n the size of the original formula, where n is the nesting of operators. However, if the depth of the query formula is considerably smaller than the size of the knowledge base, compiling the query into reduced QNF is more attractive than compiling to PINF.

Conclusions and future work

In this paper, we introduced the notion of knowing whether into proper epistemic knowledge bases. The concept of knowing whether is not as expressive as disjunction, but adds a useful level of expressiveness into the PEKB framework. We show that for the logic Kn, we can maintain a polynomial entailment mechanism at the exponential cost of pre-compilation (as in the original PEKB definition (Lakemeyer and Lesp erance 2012)), and for the logic KDn, we can maintain the polynomial entailment query mechanism presented in more recent work (Muise et al. 2015b). In future work, we will investigate notions of group belief and knowledge in PEKBs, such as common belief and common knowledge. We will also investigate how to perform sound and complete belief update on a PEKB to ensure that it remains consistent after an update.

Acknowledgements The authors thank Gerhard Lakemeyer for his insightful ideas and discussions on the knowing whether operator. This research is partially funded by Australian Research Council Discovery Grant DP130102825, Foundations of Human-Agent Collaboration: Situation-Relevant Information Sharing.

Aloni, M.; Egr e, P.; and De Jager, T. 2013. Knowing whether A or B. Synthese 190(14):2595 2621. Baier, J. A.; Mombourquette, B.; and Mc Ilraith, S. A. 2014. Diagnostic problem solving via planning with ontic and epistemic goals. In Proceedings of the Fourteenth International Conference Principles of Knowledge Representation and Reasoning, 388 397. Bienvenu, M. 2008. Prime implicate normal form for ALC concepts. In AAAI, 412 417. Bienvenu, M. 2009. Prime implicates and prime implicants: From propositional to modal logic. Journal of Artificial Intelligence Research 36(1):71 128. Eberle, R. A. 1974. A logic of believing, knowing, and inferring. Synthese 26(3):356 382. Fagin, R.; Halpern, J. Y.; Moses, Y.; and Vardi, M. Y. 1995. Reasoning about knowledge, volume 4. MIT press Cambridge.

Fan, J.; Wang, Y.; and van Ditmarsch, H. 2015. Contingency and knowing whether. The Review of Symbolic Logic 8:75 107. Halpern, J. Y., and Moses, Y. 1985. A guide to the modal logics of knowledge and belief: Preliminary draft. In Proceedings of the 9th international joint conference on Artificial intelligence, 480 490. Morgan Kaufmann Publishers. Halpern, J. Y. 1995. The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic. Artificial Intelligence 75(2):361 372. Humberstone, L. 1995. The logic of non-contingency. Notre Dame Journal of Formal Logic 36(2):214 229. Konolige, K. 1983. A deductive model of belief. In IJCAI, 377 381. Kuhn, S. 1995. Minimal non-contingency logic. Notre Dame Journal of Formal Logic 36(2):230 234. Ladner, R. E. 1977. The computational complexity of provability in systems of modal propositional logic. SIAM journal on computing 6(3):467 480. Lakemeyer, G., and Lesp erance, Y. 2012. Efficient reasoning in multiagent epistemic logics. In ECAI 2012 - 20th European Conference on Artificial Intelligence., 498 503. Muise, C.; Belle, V.; Felli, P.; Mc Ilraith, S.; Miller, T.; Pearce, A.; and Sonenberg, L. 2015a. Planning over multiagent epistemic states: A classical planning approach. In The 29th AAAI Conference on Artificial Intelligence, 3327 3334. Muise, C.; Miller, T.; Felli, P.; Pearce, A.; and Sonenberg, L. 2015b. Efficient reasoning with consistent proper epistemic knowledge bases. In Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, 1461 1469. IFAAMAS. Scherl, R. B., and Levesque, H. J. 1993. The frame problem and knowledge-producing actions. In AAAI, volume 93, 689 695. Citeseer. van der Hoek, W., and Lomuscio, A. 2003. Ignore at your peril-towards a logic for ignorance. In Proceedings of the second international joint conference on Autonomous agents and multiagent systems, 1148 1149. ACM. Van Der Hoek, W., and Lomuscio, A. 2004. A logic for ignorance. In Declarative Agent Languages and Technologies. Springer. 97 108. van Ditmarsch, H., and Kooi, B. 2015. One Hundred Prisoners and a Light Bulb. Springer.