# «Abstract. We develop clausal tableau calculi for seven multimodal logics variously designed for reasoning about multi-degree belief, reasoning about ...»

Clausal Tableaux for Multimodal Logics of Belief

Rajeev Gor´1 and Linh Anh Nguyen2

e

1

The Australian National University and NICTA

Canberra ACT 0200, Australia

Rajeev.Gore@anu.edu.au

2

Institute of Informatics, University of Warsaw

ul. Banacha 2, 02-097 Warsaw, Poland

nguyen@mimuw.edu.pl

Abstract. We develop clausal tableau calculi for seven multimodal logics variously

designed for reasoning about multi-degree belief, reasoning about distributed systems

of belief and for reasoning about epistemic states of agents in multi-agent systems.

Our tableau calculi are sound, complete, cut-free and have the analytic superformula property, thereby giving decision procedures for all of these logics. We also use our calculi to obtain complexity results for ﬁve of these logics. The complexity of one was known and that of the seventh remains open.

Keywords: modal logics for agent-based systems, theorem proving for modal logics, complexity and decidability of modal and temporal logics.

1 Introduction Modal logics have been widely studied for reasoning about knowledge and belief, usually based on the monomodal logics S 5 and KD45 for reasoning about knowledge and belief respectively. Both logics have the axioms 4 : 2ϕ → 22ϕ and 5 : ¬2ϕ → 2¬2ϕ, which mean that knowledge and belief both satisfy positive and negative introspection. The logic S 5 also has the axiom T : 2ϕ → ϕ, which means that knowledge is veridical, while KD45 also has the axiom D : 2ϕ → ¬2¬ϕ, which means that belief is consistent.

For multiple agents, the usual solution is to use a multimodal logic which has m pairs of modal operators 2i and 3i, for some ﬁxed number m. The base multimodal logics for reasoning about knowledge and belief are typically S5(m) and KD45(m), respectively, where each pair 2i and 3i is of type S5 and KD45, usually with no interactions between modal operators of diﬀerent indices (see, e.g., [14, 8, 22, 35]). An alternative is to use S 5 and KD45 type modalities labelled with agent terms [10], again without interaction axioms.

When the knowledge and beliefs of multiple agents interact then interactions between the modalities are used. One approach is to use bi-modal logics with inter- actions [33, 27]. Another is to extend the multimodal grammar logics of Fari˜as del n Cerro and Penttonent [5] with (seriality) axioms D for reasoning about knowledge and belief. Recall that a grammar logic is a multimodal logic with axioms of the form [s1 ]... [sn ]ϕ → [t1 ]... [tm ]ϕ, where [si ] and [tj ] are universal (box-like) modal operators labelled by constants si and tj, respectively (see [2, 3, 6, 34, 16, 7, 12]).

National ICT Australia (NICTA) is funded through the Australian Government’s Backing Australia’s Ability initiative, in part through the Australian Research Council.

For knowledge distributed over groups of agents there is the well-known multimodal logic of common knowledge and distributed knowledge among a group of agents (see [14, 8, 22]) as well as a similar logic for reasoning about mutual beliefs of agents [1]. There are also multi-modal logics of dynamic belief and knowledge for use in multi-agent systems [20, 32].

We concentrate on seven speciﬁc multimodal logics of belief, studied by Nguyen in the context of modal logic programming and modal deductive databases [28, 30].

**They are introduced in Section 2.2 as:**

KDI4, KDI4s, KDI4s 5, KDI45 for reasoning about multi-degree belief;

KD4s 5s for reasoning about distributed systems of belief; and KD45(m), KD4Ig 5a for reasoning about epistemic states of agents in multi-agent systems.

All except KD45(m) contain interaction axioms. Both KDI4 and KDI4s are grammar logics extended with axiom D.

Tableau methods have been successively applied to modal logics to give decision procedures (see, e.g., [9, 13, 3, 35, 11, 19, 18]). There are also tableau calculi for a number of multimodal logics of knowledge and/or belief, e.g., [3, 35, 10]. But [3] concerns only grammar logics, while [35, 10] lack interaction axioms between modal operators of diﬀerent indices. As far as we know, only KDI4 and KD45(m) from the seven multimodal logics (listed above) have labelled tableau calculi [3, 35]. We know of no non-labelled tableau calculi for any of these logics although Shvarts’ calculus for KD45 from [11] can be extended trivially to KD45(m). Nor do we know of any tableau calculus for the multimodal logic of mutual belief introduced by Aldewereld et al. [1], which is similar to our KD4s 5s.

Here, we develop (non-labelled) tableau calculi for all seven of the above multimodal logics of belief. Our tableau calculi are sound, complete, cut-free and have the analytic superformula property, so they are decision procedures.

Our tableau calculi require clausal form and are called clausal tableau calculi.

Transformation to clauses was ﬁrst used for sequent calculi by Mints [23] and Hudelmaier [17] and then applied to tableau calculi by Nguyen [24]. Hudelmaier and Nguyen showed that clausal form can give better space bounds and improved decision procedures for some modal logics [17, 24]. We show that clauses can also simplify the task of developing tableau calculi for certain modal logics by giving clausal tableau calculi for the complicated logics KDI45 and KD4Ig 5a. Finally, we show that our tableaux can be used to estimate the complexity of the satisﬁability problem in ﬁve of the multimodal logics we consider: NP-complete for KDI4s 5, KD4s 5s, KDI45, and PSPACE-complete for KDI4 and KDI4s. The complexity for KD45(m) is known to be PSPACE-complete [14]. We do not have an exact complexity result for KD4Ig 5a.

The rest of this paper is organized as follows. In Section 2, we specify the seven multimodal logics of belief and give deﬁnitions for tableau calculi. In Section 3, we deﬁne modal clauses and consider transformation to clauses. In Section 4, we present our tableau calculi and prove their soundness. In Section 5, we prove completeness of the calculi. Section 6 deals with the complexity of the logics. Section 7 contains concluding remarks.

2.1 Deﬁnitions for Multimodal Logics We consider multimodal logics with m pairs of modal operators 2i and 3i, where 1 ≤ i ≤ m. We use p and q to denote primitive propositions. Formulae of our language

**are recursively deﬁned using the BNF grammar below:**

We say that ϕ is satisﬁed at w in M if M, w ϕ. We say that ϕ is satisﬁed in M, and write M ϕ, and call M a model of ϕ, if M, τ ϕ.

If we allow all Kripke models (with no restrictions on the accessibility relations) then we obtain a multimodal logic which has a standard Hilbert-style axiomatisation denoted by K(m). Other normal multimodal logics are obtained by adding certain axioms to K(m).

Suppose a normal ﬁrst-order deﬁnable modal logic L is characterised by a class C of Kripke frames. The ﬁrst order formulae describing C are L-frame restrictions, and any frame in C is an L-frame. A model M is an L-model if its underlying frame is an L-frame. We say that ϕ is L-satisﬁable if there exists an L-model of ϕ, i.e. an L-model satisfying ϕ. A formula ϕ is said to be L-valid and called an L-tautology if ϕ is true in every L-model.

In the above systems, the axiom (I) gives 2i ϕ the meaning “ϕ is believed up to degree i”, and 3i ϕ can be read as “it is possible weakly at degree i that ϕ”. The axioms (5) are controversial as they are quite strong. For this reason, we consider also KDI4 and KDI4s. Note that the axiom (5s ) is derivable in KDI4s 5.

Although the logic KDI4 belongs to the class of logics considered by Debart et al. [4] (for multimodal logic programming) and the axioms I and 4s are possible axioms for grammar logics, the reading of modal indices as degrees of belief has not been considered by other authors. Our logics of multi-degree belief are similar to graded modal logics [22], where grades constrain the number of worlds accessible from the current world, but our degrees of belief are symbolic rather than numeric.

For multi-agent systems, we use subscripts on 2 and 3 to denote agents and assume that 2i ϕ stands for “agent i believes that ϕ is true” and 3i ϕ stands for “ϕ is considered possible by agent i”. For distributed systems of belief we can use the logic system KD4s 5s = K(m) + (D) + (4s ) + (5s ) In this system, all agents have full access to the belief bases of other agents: they are united as “friends”. Our logic KD4s 5s has features similar to the logic S5P(m) introduced by Meyer and van der Hoek [21], but S5P(m) is intended for formalising preference and the operators Pi of [21] need not be serial.

In another kind of multi-agent system, agents are “opponents” who play against each other, and each agent may want to simulate the epistemic states of the others.

To write a program for one agent, we may need to use modal operators of the other

**agents. A suitable logic for this problem is:**

** KD45(m) = K(m) + (D) + (4) + (5)**

As mentioned earlier, the logic KD45(m) has been intensively studied. We use a subscript in KD45(m) to distinguish the logic from the monomodal logic KD45, while there is not such a need for the other considered multimodal logics.

To capture common belief of a group of agents, one can extend the logic KD45(m) with modal operators for groups of agents and some additional axioms. Suppose that there are n agents and m = 2n − 1. Let g be an one-to-one function that maps every natural number less than or equal to m to a non-empty subset of {1,..., n}.

Suppose that an index 1 ≤ i ≤ m stands for the group of agents whose indices form the set g(i). We can adopt the axioms (D), (4), and additionally (Ig ) : 2i ϕ → 2j ϕ if g(i) ⊃ g(j), so i indicates a group that contains the group identiﬁed by j, and (5a ) : ¬2i ϕ → 2i ¬2i ϕ if g(i) is a singleton, so that i stands for an agent. Thus, for

**reasoning about belief and common belief, we can use:**

** KD4Ig 5a = K(m) + (D) + (4) + (Ig ) + (5a )**

4 Here we want to catch the most important properties of belief and common belief, and the aim is not to give an exact formulation of belief or common belief. This logic is therefore diﬀerent in nature from the well-known multimodal logics of common knowledge with ﬁxed-points. It also diﬀers from the multimodal logic of mutual belief introduced by Aldewereld et al. [1]. Our modal operator of common belief satisﬁes positive introspection, while the operator of mutual belief introduced in [1] lacks this property. On the other hand, the latter operator has some properties that the former does not have.

**The given axioms correspond to the following frame restrictions:**

2.3 Deﬁnitions for Tableau Calculi As in our previous works on tableau calculi [11, 27, 12], our tableau formulation traces their roots to Hintikka via [31]. A tableau rule σ consists of a numerator N above the line and a (ﬁnite) list of denominators D1, D2,..., Dk (below the line) separated by vertical bars. The numerator is a ﬁnite formula set, and so is each denominator. As we shall see later, each rule is read downwards as “if the numerator is L-satisﬁable, then so is one of the denominators”. The numerator of each tableau rule contains one or more distinguished formulae called the principal formulae. A tableau calculus CL for a logic L is a ﬁnite set of tableau rules.

A CL-tableau for X is a tree with root X whose nodes carry ﬁnite formula sets obtained from their parent nodes by instantiating a tableau rule with the proviso that if a child s carries a set Z and Z has already appeared on the branch from the root to s then s is an end node.

Let ∆ be a set of tableau rules. We say that Y is obtainable from X by applications of rules from ∆ if there exists a tableau for X which uses only rules from ∆ and has a node that carries Y. A branch in a tableau is closed if its end node carries only ⊥.

A tableau is closed if every one of its branches is closed. A tableau is open if it is not closed. A ﬁnite formula set X is CL-consistent if every CL-tableau for X is open. If there is a closed CL-tableau for X then X is CL-inconsistent.

A tableau calculus CL is sound if for all ﬁnite formula sets X, if X is L-satisﬁable then X is CL-consistent. It is complete if for all ﬁnite formula sets X, if X is CLconsistent then X is L-satisﬁable. Let σ be a rule of CL. We say that σ is sound w.r.t. L if for every instance σ of σ, if the numerator of σ is L-satisﬁable then so is one of the denominators of σ. Any CL containing only rules sound w.r.t. L is sound.

** 53 Modal Clauses**

A classical literal is a formula of the form p or ¬p, where p is a primitive proposition.

We use a, b, c to denote classical literals, and to denote a possibly empty sequence of universal (box-like) modal operators, which is also called a universal modality. We write [ϕ1,..., ϕk ] to denote (ϕ1 ∨... ∨ ϕk ) with the emphasis that the order of disjuncts is not important.

A (modal) clause is a formula of the form [a1,..., ak ], [a, 2i b], [a, 3i b], or 3i b, where is called the modal context.

Proposition 1. Every formula set can be transformed in quadratic time to a set of clauses which is equisatisﬁable in any normal modal logic to the ﬁrst set.

Proof. Repeatedly replace a complex formula by a new primitive proposition which is “deﬁned” by that formula (see, e.g., [23, 17, 24]). For example, (ϕ ∨ 3i ψ), where ψ is not a primitive proposition, is replaced by (ϕ ∨ 3i p) and 2i (¬p ∨ ψ), where p is a fresh primitive proposition (deﬁning ψ via the second added clause). We need to do at most n such replacements, where n is the sum of the lengths of formulae belonging to the input set. Hence the transformation can be done in quadratic time.

**We now deﬁne L-clauses using a case-distinction on L as:**

For L ∈ {KDI4, KDI4s, KD4Ig 5a }: every clause is an L-clause;

For L ∈ {KD4s 5s, KDI4s 5}: an L-clause is a clause with modal depth 1 or 0;