Emiliano Lorini
email: emiliano.lorini@irit.fr

Exploiting Belief Bases for Building Rich Epistemic Structures

We introduce a semantics for epistemic logic exploiting a belief base abstraction. Differently from existing Kripke-style semantics for epistemic logic in which the notions of possible world and epistemic alternative are primitive, in the proposed semantics they are non-primitive but are defined from the concept of belief base. We show that this semantics allows us to define the universal epistemic model in a simpler and more compact way than existing inductive constructions of it. We provide (i) a number of semantic equivalence results for both the basic epistemic language with 'individual belief' operators and its extension by the notion of 'only believing', and (ii) a lower bound complexity result for epistemic logic model checking relative to the universal epistemic model.

Introduction

Type spaces were introduced by Harsanyi [START_REF] Harsanyi | Games with incomplete information played by 'Bayesian' players[END_REF] in order to formally represent higher-order probabilistic beliefs of rational players in strategic situations. The notion of universal type space was studied in detail by Mertens & Zamir [START_REF] Mertens | Formulation of Bayesian analysis for games with incomplete information[END_REF]: it is defined to be the "largest" type space which contains all possible states of the world as well as all possible belief hierarchies of the players. Mertens & Zamir showed that, under certain topological assumptions, every Harsanyi type space can be mapped to the universal type space by a morphism which preserves the current state of the world as well as the players' belief hierarchies. Alternative constructions of the universal type space under different topological assumptions can be found in [START_REF] Brandenburger | Hierarchies of Beliefs and Common Knowledge[END_REF][START_REF] Heifetz | The Bayesian formulation of incomplete information: the non-compact case[END_REF]. Heifez & Samet [START_REF] Heifetz | Topology-Free Typology of Beliefs[END_REF] proved a variant of Mertens & Zamir's result for the general measure-theoretic case. Battigalli & Siniscalchi [START_REF] Battigalli | Hierarchies of Conditional Beliefs and Interactive Epistemology in Dynamic Games[END_REF] extended the universal type space construction to conditional probabilistic beliefs. More recently, Bjorndahl & Halpern [START_REF] Bjorndahl | From Type Spaces to Probability Frames and Back, via Language[END_REF] provided a logical analysis of the probabilistic structure of the universal type space. 1A qualitative version of the universal type space was introduced by Fagin et al. [START_REF] Fagin | A Model-Theoretic Analysis of Knowledge[END_REF] (see also [START_REF] Fagin | The Hierarchical Approach to Modeling Knowledge and Common Knowledge[END_REF]). Specifically, Fagin et al. provided a construction of the "largest" (or "universal") epistemic model for the epistemic logic S5 n which contains all possible knowledge hierarchies of the agents in the system. They studied its relationship with the standard multi-relational semantics of epistemic logic [START_REF] Fagin | Reasoning about Knowledge[END_REF] both for the basic epistemic language with 'individual knowledge' operators and for its extension by common knowledge operators.

Both constructions of the universal epistemic model in its probabilistic version à la Mertens & Zamir and in its qualitative version à la Fagin et al. are inductive. One has to define first the set of possible states of the world. Then, the agents' first-order beliefs about the states of the world are defined. In the third step, one has to define the agents' second-order beliefs about the states of nature and the agents' first-order beliefs, and so on so forth. More generally, in order to define an agent's k + 1-order belief one has to define first the agents' k-order beliefs.

The general aim of the present paper is to offer a simple and compact construction of the universal epistemic model that does not require an inductive construction of the agents' belief hierarchies, as in Mertens & Zamir's and Fagin et al.'s definitions. Our construction of the universal epistemic model is based on a semantics for epistemic logic exploiting a belief base abstraction which was recently introduced in [START_REF] Lorini | In Praise of Belief Bases: Doing Epistemic Logic Without Possible Worlds[END_REF]. Differently from existing multi-relational Kripke semantics for epistemic logic in which the notions of possible world and epistemic alternative are primitive, in the belief base semantics they are non-primitive but are defined from the concept of belief base. Specifically, in this semantics it is assumed that at a given state s agent i considers state s possible if and only if s satisfies all formulas that are included in agent i's belief base at s.

The initial motivation for introducing such a semantics was to bridge two traditions that have rarely talked to each other in the past. On the one hand, we have epistemic logic: it started in the 60s with the seminal work of Hintikka [START_REF] Hintikka | Knowledge and Belief. An introduction to the logic of the two notions[END_REF] on the logics of knowledge and belief, it was extended to the multi-agent setting at the end of 80s [START_REF] Fagin | Reasoning about Knowledge[END_REF][START_REF] Meyer | Epistemic Logic for AI and Theoretical Computer Science[END_REF] and then furtherly developed during the last 20 years, the period of the "dynamic turn", with growing research on dynamic epistemic logic [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF]. On the other hand, we have syntactic approaches to knowledge representation and reasoning mainly proposed in the area of artificial intelligence (AI). The latter includes, for instance, work on belief base and knowledge base revision [START_REF] Hansson | Theory contraction and base contraction unified[END_REF][START_REF] Hansson | A Textbook of Belief Dynamics: Theory Change and Database Updating[END_REF][START_REF] Benferhat | A practical approach to revising prioritized knowledge bases[END_REF], belief base merging [START_REF] Konieczny | Merging information under constraints: a logical framework[END_REF], input-output logic [START_REF] Makinson | Input/output logics[END_REF], as well as more recent work on the socalled "database perspective" to the theory of intention by [START_REF] Shoham | Logical Theories of Intention and the Database Perspective[END_REF]. All these approaches defend the idea that right level of abstraction for modeling rational agents is the "belief base" (or "knowledge base") level whereby the agent is identified with the set of facts that she believes (or knows).

The paper is organized as follows. In Section 2, we present the belief base semantics for epistemic logic, as defined in [START_REF] Lorini | In Praise of Belief Bases: Doing Epistemic Logic Without Possible Worlds[END_REF][START_REF] Lorini | Decision procedures for epistemic logic exploiting belief bases[END_REF]. We show how the basic language with 'individual belief' operators can be interpreted on this semantics. We also show how the semantics can be easily incorporate the belief correctness assumption, thereby allowing us to model knowledge instead of belief. We show that the belief base semantics is equivalent to the standard multi-relational Kripke semantics, in the sense that they lead to the same set of validities. Section 3 is the core of the paper: we define the universal epistemic model with the help of the belief base semantics. As emphasized above, our definition is simpler and more compact than existing definitions of the universal epistemic model, since it does not require an inductive construction of the agents' belief hierarchies. We show that, as far as the basic epistemic language with 'individual belief' operators is concerned, the set of validities relative to the universal epistemic model and the set of validities relative to the generic belief base semantics are the same. In Section 4, we extend the basic epistemic language by the notion of 'only believing'. We show that the equivalence between the two semantics does not hold anymore in the context of this more expressive language: the universal epistemic model has more validities than the generic belief base semantics. Section 5 is devoted to the comparison between Fagin et al.'s inductive construction of the universal epistemic model and the construction of Section 3 exploiting belief bases. In particular, we show that, from the point of the basic epistemic language and of its extension by the notion of 'only believing', there is no difference between the two constructions, as they give rise to the same set of validities. In Section 6, we provide a compact formulation of epistemic logic model checking which exploits the definition of the universal epistemic model given in Section 3. We show that such a compact formulation makes epistemic logic model checking PSPACE-hard, whereas standard epistemic logic model checking relative to the multirelational Kripke semantics is polynomial in the size of the model and the length of the formula. In Section 7, we conclude.

Belief base semantics for epistemic logic

In this section, we present a semantics for epistemic logic (EL) in which the accessibility relations in an epistemic model are not primitive but they are defined from the primitive concept of multi-agent belief base. The semantics was first introduced in [START_REF] Lorini | In Praise of Belief Bases: Doing Epistemic Logic Without Possible Worlds[END_REF].

Multi-agent belief base models

Assume a countably infinite set of atomic propositions Atm = {p, q, . . .} and a finite set of agents Agt = {1, . . . , n}.

We define the language L 0 (Atm, Agt) by the following grammar in Backus-Naur Form (BNF):

α ::= p | ¬α | α 1 ∧ α 2 | i α
where p ranges over Atm and i ranges over Agt. L 0 (Atm, Agt) is the language for representing explicit beliefs of multiple agents. For simplicity, we sometimes write L 0 instead of L 0 (Atm, Agt), when the context is unambiguous. The formula i α can be read as "agent i explicitly believes that α is true" or "α is in agent i's belief base". In this language, we can represent higher-order explicit beliefs, for example i j α express the fact that agent i explicitly believes that agent j explicitly believes that α is true.

Definition 1 (Multi-agent belief base). A multi-agent belief base (MBB) is a tuple B = (B 1 , . . . , B n , V) where (i) for every i ∈ Agt, B i ⊆ L 0 is agent i's belief base, and (ii) V ⊆ Atm is the actual state. The class of MBBs is denoted by B.

Formulas of the language L 0 are interpreted relative to MBBs as follows.

Definition 2 (Satisfaction relation for formulas in L 0 ). Let B = (B 1 , . . . , B n , V) ∈ B. Then, the satisfaction relation |= between B and formulas in L 0 is defined as follows: A multi-agent belief model (MAB) is defined to be a multi-agent belief base supplemented with a set of multi-agent belief bases, called context. The latter includes all multi-agent belief bases that are compatible with the agents' common ground [START_REF] Stalnaker | Common ground[END_REF], i.e., the body of information that the agents commonly believe to be the case.

B |= p ⇐⇒ p ∈ V B |= ¬α ⇐⇒ B |= α B |= α 1 ∧ α 2 ⇐⇒ B |= α 1 and B |= α 2 B |= i α ⇐⇒ α ∈ B i Definition 3 (Correct MBB). Let B = (B 1 , . . . , B n , V) ∈ B.

Interpretation of epistemic logic language

Thanks to the epistemic accessibility relations defined in Definition 4, we are able to interpret the language of epistemic logic relative to MBMs. Such language is denoted by L EL (Atm, Agt) and is defined by the following grammar:

ϕ ::= p | ¬ϕ | ϕ 1 ∧ ϕ 2 | i ϕ
where p ranges over Atm and i ranges over Agt. For simplicity, we write L EL instead of L EL (Atm, Agt), when the context is unambiguous. The other Boolean constructions , ⊥, ∨, → and ↔ are defined from p, ¬ and ∧ in the usual way.

The formula i ϕ has to be read "agent i implicitly (or potentially) believes that ϕ is true" in the sense that agent i can derive ϕ from her explicit beliefs (i.e., from the information in her belief base). For the sake of simplicity, we sometimes read the formula i ϕ as "agent i believes that ϕ". We define the dual operator ♦ i as follows:

♦ i ϕ def = ¬ i ¬ϕ.
♦ i ϕ has to be read "ϕ is compatible (or consistent) with agent i's explicit beliefs".

As usual, for every formula ϕ ∈ L EL we denote by Atm(ϕ) the set of atoms in Atm occurring in ϕ.

We are ready to define what it means for a multi-agent belief model (MBM) (B, Cxt) to satisfy a formula ϕ in L EL , written (B, Cxt) |= ϕ.

Definition 6 (Satisfaction relation for formulas in

L EL ). Let B = (B 1 , . . . , B n , V) ∈ B and let (B, Cxt) ∈ M. Then: (B, Cxt) |= p ⇐⇒ p ∈ V (B, Cxt) |= ¬ϕ ⇐⇒ (B, Cxt) |= ϕ (B, Cxt) |= ϕ ∧ ψ ⇐⇒ (B, Cxt) |= ϕ and (B, Cxt) |= ψ (B, Cxt) |= i ϕ ⇐⇒ ∀B ∈ Cxt : if BR i B then (B , Cxt) |= ϕ
Note that, according to the last clause, an agent i implicitly believes that ϕ (i.e., i ϕ) if and only if ϕ is true at all states that are compatible with the information in i's belief base.

Figure 1 illustrates the general idea behind the belief base semantics, especially for what concerns the relationship between the agents' belief bases and the agents' common ground (or context) and the relationship between the latter and the agents' implicit beliefs. While an agent's belief base captures the agent's private information, the common ground captures the agents' public information. An agent's implicit belief corresponds to a fact that the agent can deduce from the public information and her private information.

Given a formula ϕ in L EL , we denote by depth(ϕ) its model depth which is defined as follows:

depth(p) = 0 depth(¬ϕ) = depth(ϕ) depth(ϕ ∧ ψ) = max depth(ϕ), depth(ψ) depth( i ϕ) = depth(ϕ) + 1

Model classes and validity

In some situations, it may be useful to assume that agents' beliefs are correct, i.e., what an agent believes is true. When talking about correct (or true) explicit and implicit beliefs, it is usual to call them explicit and implicit knowledge. Indeed, we assume that the terms "true belief", "correct belief" and "knowledge" are synonyms. The following definition introduces belief correctness for multi-agent belief models.

Definition 7 (Belief correctness). Let (B, Cxt) ∈ M. We say that (B, Cxt) satisfies belief correctness (BC) if and only if B ∈ Cxt and, for every B ∈ Cxt, B R i B .

As the following proposition highlights, belief correctness for multi-agent belief models is completely characterized by the fact that the actual world is included in the agents' common ground and that the agents' explicit beliefs are correct, i.e., if an agent has α in her belief base then α is true in the actual state of the world. We let M BC denote the class of MBMs satisfying property BC. Let ϕ ∈ L EL , we say that ϕ is valid for the class M, denoted by |= M ϕ, if and only if, for every (B, Cxt) ∈ M, we have (B, Cxt) |= ϕ. We say that ϕ is satisfiable for the class M if and only if ¬ϕ is not valid for the class M. Satisfiability and validity of a formula ϕ in L EL relative to the class M BC (denoted by |= M BC ϕ) are defined in an analogous way.

Equivalence with Kripke semantics

In this section, we show that the belief base semantics for the epistemic language L EL defined in the previous section is equivalent to the traditional multi-relational Kripke semantics for epistemic logic [START_REF] Fagin | Reasoning about Knowledge[END_REF].

Definition 9 (Multi-relational Kripke model).

A multi-relational Kripke model is a structure M = (W, ⇒ 1 , . . . , ⇒ n , ω) such that W is a set of states, ⇒ i ⊆ W ×W is agent i's epistemic accessibility relation, and ω : Atm -→ 2 W is a valuation function. Multi-relational Kripke models satisfying reflexivity are those for which every relation ⇒ i is reflexive (i.e., for every w ∈ W , w ⇒ i w).

The interpretation of formulas in L EL relative to a multi-relational Kripke model M = (W, ⇒ 1 Exploiting Belief Bases for Building Rich Epistemic Structures , . . . , ⇒ n , ω) and a world w in W is defined as follows:

(M, w) |= p iff w ∈ ω(p) (M, w) |= ¬ϕ iff (M, w) |= ϕ (M, w) |= ϕ ∧ ψ iff (M, w) |= ϕ and (M, w) |= ψ (M, w) |= i ϕ iff ∀v ∈ W : if w ⇒ i v then (M, v) |= ϕ
Notions of validity and satisfiability relative to the class of multi-relational Kripke models are defined in the usual way. We denote the fact that ϕ is valid relative to the class of multi-relational Kripke models (resp. multi-relational Kripke models satisfying reflexivity) by |= KripkeM ϕ (resp. |= ReflKripkeM ϕ).

The equivalence between the belief base semantics for the language L EL and the multi-relational Kripke semantics is stated by the following theorem. Theorem 10. Let ϕ ∈ L EL . Then,

• |= M ϕ if and only if |= KripkeM ϕ,

• |= M BC ϕ if and only if |= ReflKripkeM ϕ.

Universal context

We here define the notion of universal context, as the context containing all possible explicit belief hierarchies for the agents. Definition 11 (α-context). Let α ∈ L 0 . We define

B α = {B ∈ B : B |= α}
to be the α-context. The universal context is simply B which is the same thing as B.

The formula α in the previous definition corresponds to the concept of integrity constraint, as traditionally defined in the area of knowledge representation [START_REF] Reiter | On integrity constraints[END_REF][START_REF] Konieczny | Merging information under constraints: a logical framework[END_REF].

It is worth to consider a more specific notion of universal context under the assumption of belief correcteness. Definition 12 (α-context with belief correctness). Let α ∈ L 0 . We define

CB α = {B ∈ CB : B |= α}
to be the α-context with belief correctness. The universal context with belief correctness is simply CB which is the same thing as CB.

Let ϕ ∈ L EL , we say that ϕ is valid relative to the universal context B , denoted by |= B ϕ, if and only if, for every B ∈ B , we have (B, B ) |= ϕ. Analogously, we say that ϕ is valid relative to the universal context satisfying BC, denoted by |= CB ϕ, if and only if, for every B ∈ CB , we have

(B, CB ) |= ϕ.
We say that ϕ is satisfiable relative to the universal context B (resp. CB ) if and only if ¬ϕ is not valid relative to the universal context B (resp. CB ).

The following theorem highlights that the set of validities for the language L EL relative to the universal context B (resp. CB ) and the set of validities relative to the class of models M (resp. M BC ) are the same. In other words, the language L EL is not able to distinguish the universal context including all possible hierarchies of the agents' beliefs from incomplete models in which some belief hierarchy may be missing. The notion of universal context allows us to easily define the notion of model with maximal general uncertainty, that is, to say a model in which the agents have maximal uncertainty about the state of the world as well as maximal uncertainty about the agents' k-order beliefs for every k ≥ 1, where the order of a belief is defined inductively as follows: (i) an agent's belief is order 1 if and only if its content is a propositional formula that does not mention beliefs; (ii) an agent's belief is order k + 1 if and only it is a belief about the agents' k-order beliefs.

Definition 15 (MBM with maximal general uncertainty). Let B = (B 1 , . . . , B n , V) ∈ B such that B i = / 0 for every i ∈ Agt. Then, (B, B ) is called MBM with maximal general uncertainty, while (B, CB ) is called MBM with maximal general uncertainty and belief correctness.

Note that in our semantics maximal general uncertainty coincides with the fact that the agents' belief bases are empty (i.e., the agents do not know anything). The following proposition is a direct consequence of Theorem 13. It highlights the essential aspects of models with maximal general uncertainty. To see this, suppose ϕ and ¬ϕ are both satisfiable for the class M (resp. for the class M BC ). Then, by Proposition 16, we have

(B, B ) |= ♦ i ϕ ∧ ♦ i ¬ϕ (resp. (B, CB ) |= ♦ i ϕ ∧ ♦ i ¬ϕ)
, where ♦ i ϕ ∧ ♦ i ¬ϕ captures agent i's uncertainty about ϕ. More generally, for every formula ϕ yielding information either about the state of the world or about the agents' higher-order beliefs, if ϕ and ¬ϕ are both satisfiable, then in a model with maximal uncertainty every agent i has uncertainty about ϕ.

Only believing

The aim of this section is to show that if we increase the expressive power of our multimodal epistemic language by the notions of 'believing at most' and 'only believing', then the equivalence result between the generic semantics in terms of MBMs and the universal context semantics of Section 3 does not hold anymore.

Let L EEL (Atm, Agt) be the language which extends language L EL by modal operators of implicitly believing 'at most' of the form ∇ i , where EEL stands for "Extended Epistemic Logic". It is defined by the following grammar:

ϕ ::= p | ¬ϕ | ϕ 1 ∧ ϕ 2 | i ϕ | ∇ i ϕ
where p ranges over Atm and i ranges over Agt. For simplicity, we write L EEL instead of L EEL (Atm, Agt), when the context is unambiguous.

The formula ∇ i ϕ has to be read "agent i believes at most that ¬ϕ" and has the following interpretation relative to MBMs.

Definition 17 (Satisfaction relation (cont.)). Let B = (B 1 , . . . , B n , V) ∈ B and let (B, Cxt) ∈ M. Then:

(B, Cxt) |= ∇ i ϕ ⇐⇒ ∀B ∈ Cxt \ R i (B) : (B , Cxt) |= ϕ where R i (B) = {B : BR i B }.
The definition of modal depth of a formula in L EEL extends the definition of the modal depth of formulas in L EL by the following additional clause:

depth(∇ i ϕ) = depth(ϕ) + 1
By combining the operators i and ∇ i in the appropriate way, we can reconstruct the universal modality [START_REF] Hemaspaandra | The Price of Universality[END_REF][START_REF] Goranko | Using the universal modality: gains and questions[END_REF]:

Uϕ def = i ϕ ∧ ∇ i ϕ
where Uϕ has to be read "ϕ is universally true". We can moreover the reconstruct the "only believing" modality [START_REF] Levesque | All I know: a study in autoepistemic logic[END_REF][START_REF] Halpern | Multi-agent only knowing[END_REF][START_REF] Lakemeyer | All they know: a study in multi-agent autoepistemic reasoning[END_REF]:

O i ϕ def = i ϕ ∧ ∇ i ¬ϕ
where O i ϕ has to be read "all that agent i believes is ϕ". From the perspective of the logic of only believing, all that agent i believes is ϕ if and only if agent i believes at least that ϕ is true (i.e., i ϕ) and she believes at most that ϕ is true (i.e., ∇ i ¬ϕ).

Definitions of validity and satisfiability for formulas in L EEL relative to the class M (resp. M BC ) and relative to the universal context B (resp. CB ) coincide with those for formulas in L EL given above.

The following theorem highlights that the semantics for the language L EEL based on the universal context contains more validities than the semantics for the language L EEL based on the generic class M. Theorem 18. We have the following relationship between sets of validities: The following is a direct consequence of Theorems 18 and 19.

• {ϕ ∈ L EEL :|= M ϕ} ⊂ {ϕ ∈ L EEL :|= B ϕ}, • {ϕ ∈ L EEL :|= M BC ϕ} ⊂ {ϕ ∈ L EEL :|= CB ϕ}. Showing that {ϕ ∈ L EEL :|= M ϕ} ⊆ {ϕ ∈ L EEL :|= B ϕ} is trivial since (B, B ) ∈ M for every B ∈ B .
Theorem 20. We have the following relationship between sets of validities:

• {ϕ ∈ L EEL :|= KripkeM ϕ} ⊂ {ϕ ∈ L EEL :|= B ϕ}, • {ϕ ∈ L EEL :|= ReflKripkeM ϕ} ⊂ {ϕ ∈ L EEL :|= CB ϕ}.

Qualitative belief structures

In this section, we consider a different representation of the universal epistemic model containing all possible belief hierarchies for the agents in the system first proposed by [START_REF] Fagin | A Model-Theoretic Analysis of Knowledge[END_REF] (see also [START_REF] Fagin | The Hierarchical Approach to Modeling Knowledge and Common Knowledge[END_REF]). Differently from the definition of the universal context given in Section 3, which does not require any inductive construction of belief hierarchies, Fagin et al.'s definition of the universal epistemic model is inductive. As emphasized by [START_REF] Van Benthem | Logics for Analyzing Games[END_REF], Fagin et al.'s universal epistemic model can be seen as qualitative counterpart of the notion of probabilistic universal type space by [START_REF] Mertens | Formulation of Bayesian analysis for games with incomplete information[END_REF]. A similar inductive construction of the universal epistemic model was proposed more recently by [START_REF] Belle | Multi-Agent Only-Knowing Revisited[END_REF] (see also [START_REF] Aucher | Multi-Agent Only Knowing on Planet Kripke[END_REF]), as a semantics for the logic of multiagent only knowing.

Fagin et al. study the universal epistemic model for the multimodal logic S5 n , including both positive and negative introspection principles for knowledge. We here consider variants of Fagin et al.'s construction for the multimodal logics K n and KT n , the latter including the veracity principle for knowledge according to which what an agent knows cannot be false. 2Given an arbitrary set Y , let F(Y ) be the set of functions with domain Y and codomain {0, 1}. We define the set Z k in an inductive way as follows:

Z 0 =F(Atm) Z k+1 =Z k × F(Z k ) n .
Thus, we have

Z k+1 =Z 0 × F(Z 0 ) n × . . . × F(Z k ) n .
Elements of Z 0 are denoted by f 0 , while elements of F(Z k ) n are denoted by f k+1 , f k+1 , . . . Moreover, for every i ∈ Agt and for every f k+1 ∈ F(Z k ) n , f k+1 (i) denotes the i-th component in the tuple f k+1 .

Elements of Z k are called k + 1-ary worlds, or simply k + 1-worlds. Elements of k∈N 0 Z k are called worlds. The set of worlds is denoted by W.

The set of belief structures is defined as follows:

BS =Z 0 × F(Z 0 ) n × F(Z 1 ) n × . . .
Thus, a belief structure is a countably infinite sequence f = ( f 0 , f 1 , . . .) such that f 0 ∈ Z 0 and, for every

k ∈ N 0 , f k+1 ∈ F(Z k ) n . It follows that f = ( f 0 , f 1 , . . .) is a belief structure if and only if, for every k ∈ N 0 , ( f 0 , . . . , f k ) is a k + 1-world.
Definition 21 (Coherent world and belief structure). A world ( f 0 , . . . , f k ) is said to be coherent if and only if, the following conditions hold:

• for every i ∈ Agt and for every 2

≤ h ≤ k: if f h (i)(g 0 , . . . , g h-1 ) = 1 then f h-1 (i)(g 0 , . . . , g h-2 ) = 1;
• for every i ∈ Agt and for every 1

≤ h ≤ k -1: if f h (i)(g 0 , . . . , g h-1 ) = 1 then there exists g h ∈ F(Z h-1 ) n such that f h+1 (i)(g 0 , . . . , g h-1 , g h ) = 1.
The set of coherent worlds is denoted by CW. We say that the belief structure f = ( f 0 , f 1 , . . .) is coherent if, for every k ∈ N 0 , ( f 0 , . . . , f k ) is a coherent world. The set of coherent belief structures is denoted by CBS.

The following definition introduces the property of correctness for worlds and belief structures. A formula ϕ of the language L EEL is interpreted relative to a coherent k + 1-world ( f 0 , . . . , f k ) ∈ CW such that k ≥ depth(ϕ), as follows:

( f 0 , . . . , f k ) |= p ⇐⇒ f 0 (p) = 1 ( f 0 , . . . , f k ) |= ¬ϕ ⇐⇒ ( f 0 , . . . , f k ) |= ϕ ( f 0 , . . . , f k ) |= ϕ ∧ ψ ⇐⇒ ( f 0 , . . . , f k ) |= ϕ and ( f 0 , . . . , f k ) |= ψ ( f 0 , . . . , f k ) |= i ϕ ⇐⇒ ∀(g 0 , . . . , g k-1 ) ∈ Z k-1 : if f k (i)(g 0 , . . . , g k-1 ) = 1 then (g 0 , . . . , g k-1 ) |= ϕ ( f 0 , . . . , f k ) |= ∇ i ϕ ⇐⇒ ∀(g 0 , . . . , g k-1 ) ∈ Z k-1 : if f k (i)(g 0 , . . . , g k-1 ) = 0 then (g 0 , . . . , g k-1 ) |= ϕ
The following proposition is a generalization of [START_REF] Fagin | A Model-Theoretic Analysis of Knowledge[END_REF]Lemma 2.5] to the language L EEL . 3Proposition 23. Let depth(ϕ) = h, k ≥ h, and ( f 0 , . . . , f h ), ( f 0 , . . . , f k ) ∈ CW. Then, ( f 0 , . . . ,

f h ) |= ϕ if and only if ( f 0 , . . . , f k ) |= ϕ. Let ϕ ∈ L EEL and let f = ( f 0 , f 1 , . . .) ∈ CBS be a coherent belief structure. We say that f satisfies ϕ, denoted by f |= ϕ if ( f 0 , . . . , f h ) |= ϕ where h = depth(ϕ). It is worth noting that, by Proposition 23, if k ≥ h then f |= ϕ if and only if ( f 0 , . . . , f k ) |= ϕ.
We moreover say that ϕ is valid relative to the class CBS, denoted by |= CBS ϕ, if f |= ϕ for every f ∈ CBS. We say that ϕ is satisfiable relative to the class CBS if |= CBS ¬ϕ. Definitions of validity relative to the class CBS BC (denoted by |= CBS BC ϕ) and satisfiability are defined analogously.

It is straightforward to adapt the proof of [START_REF] Fagin | A Model-Theoretic Analysis of Knowledge[END_REF][Theorem 3.1] in order to prove the following equivalence result between the coherent belief structure semantics and the Kripke semantics relative to the language L EL .

Theorem 24. Let ϕ ∈ L EL . Then,

• |= CBS ϕ if and only if |= KripkeM ϕ, • |= CBS BC ϕ if and only if |= ReflKripkeM ϕ.
The following theorem is a corollary of Theorems 14 and 24.

Theorem 25. Let ϕ ∈ L EL . Then,

• |= B ϕ if and only if |= CBS ϕ, • |= CB ϕ if and only if |= CBS BC ϕ.
The following theorem strengthens Theorem 25 by stating that the set of L EEL -validites relative to the universal context B (resp. CB ) is the same as the set of L EEL -validites relative to the class CBS (resp. CBS BC ).

Theorem 26. Let ϕ ∈ L EEL . Then,

• |= B ϕ if and only if |= CBS ϕ, • |= CB ϕ if and only if |= CBS BC ϕ.
More generally, not even the epistemic language L EEL -which extends the language L EL by the notions of 'believing at most' and 'only believing' -can distinguish the belief structure semantics à la Fagin et al. from the universal context semantics exploiting the belief base abstraction.

Model checking

The notions of α-context and universal context defined in Section 3 (Definition 11) allow us to offer a compact formulation of the model checking problem for the formulas in the language L EL . 4α-context model checking Given: ϕ ∈ L EL , α ∈ L 0 and a finite B ∈ B. Question: Do we have (B, B α ) |= ϕ?

where the multi-agent belief base (MBB) B = (B 1 , . . . , B n , V) is said to be finite if V and every B i are finite.

Note that, if α = , then model checking consists in verifying whether ϕ is true at a given finite MBB of the universal context, that is, in verifying whether (B, B ) |= ϕ for a specific finite B ∈ B .

The model checking problem for multi-agent epistemic logic K n interpreted relative to the standard multi-relational Kripke semantics of Definition 9 is known to be P-complete with respect to the size of the input formula to be checked and the size of the model [START_REF] Grädel | On logics with two variables[END_REF]. In this section, we are going to show that the previous compact formulation of the model checking problem for the formulas in L EL is PSPACEhard, the same complexity as the corresponding satisfiability problem. Our result highlights that the gains in terms of compactness of the model checking problem are counterbalanced by losses on the complexity side.

We provide a polynomial reduction of true quantified boolean formulas (TQBF) to model checking for formulas in L EL .

Let us assume that a quantified boolean formula χ is in (not necessarily closed) prenex normal form and can be written as follows:

λ .π where π is a propositional formula and λ is a (possibly empty) sequence Q 0 p 0 . . . Q m p m such that {p 0 , . . . , p m } ⊆ Atm(π) and Q 0 , . . . , Q m ∈ {∃, ∀}, with Atm(π) denoting the set of atoms occurring in π. If {p 0 , . . . , p m } = Atm(π) then χ is said to be closed, as it has no free variables. The length of χ is defined to be the length of the sequence p 0 . . . p m . For notational convenience, when λ is non empty, we write λ [k] to denote the propositional variable in the k-th position in the sequence p 0 . . . p m .

Let us suppose that the language of quantified boolean formulas is built over the set of atomic variables Atm. Moreover, let us define the following translation from the language of quantified boolean formulas to the language L EL (Atm, {1}):

tr(p) = for p ∈ Atm tr ∀pλ .π =[[λ ]]tr(λ .π)
where

[[λ ]]ψ def = 1 ( 1 λ [0] → ψ) and 1 λ [0] def = ♦ 1 λ [0] ∧ ♦ 1 ¬λ [0] if λ is non-empty 1 λ [0] def = otherwise
and where the Boolean connectives are translated homomorphically. We define the dual operator of [[λ ]] as follows:

λ ψ def = ¬[[λ ]]¬ψ.
For every quantified boolean formula χ = λ .π = Q 0 p 0 . . . Q m p m .π and for every V ⊆ Atm, we define:

Σ χ,V = (Atm(π) \ {λ [0]}) ∩ V ∪ {¬q : q ∈ (Atm(π) \ {λ [0]}) \ V}∪ 1≤k≤m { k-1 1 q∈Atm(π)\{λ [k]} ( 1 q ∨ 1 ¬q)}
where k-1 1 α is inductively defined as follows:

k-1

1 α def = α if k = 1 k-1 1 α def = 1 k-2 1 α if k > 1
Moreover, let us define

B (χ,V) = B (χ,V) 1 , V where
B (χ,V) 1 = Σ χ,V if λ is non-empty B (χ,V) 1 = / 0 otherwise
The following lemma is crucial for proving the main result of this section about complexity of model checking for formulas in L EL .

Lemma 1. Let V ⊆ Atm and let χ = λ .π be a quantified boolean formula. Then, V |= χ if and only if B (χ,V) , B |= tr(χ).

Thanks to Lemma 1 and the fact that the TQBF problem (i.e., the problem of checking whether a quantified boolean formula is true in a given valuation) is PSPACE-hard [START_REF] Stockmeyer | Word problems requiring exponential time (Preliminary Report)[END_REF], we have a PSPACEhardness result for model checking of L EL -formulas. Indeed, let χ = Q 0 p 0 . . . Q m p m .π be a quantified boolean formula. Then, the sizes of B (χ,V) 1 and tr(χ) are polynomial in m. Therefore, by Lemma 1 we have a polynomial reduction of the TQBF problem into EL-model checking. Since the former is PSPACEhard, then the latter is PSPACE-hard too.

Theorem 27. The α-context model checking problem for formulas in L EL is PSPACE-hard.

From [START_REF] Halpern | A Guide to Completeness and Complexity for Modal Logics of Knowledge and Belief[END_REF] we know that satisfiability checking for L EL -formulas relative to multi-relational Kripke models of Definition 9 is PSPACE-complete. Thus, thanks to Theorem 14, we can conclude that satisfiability checking for L EL -formulas relative to the universal context B is PSPACE-complete as well. Consequently, Theorem 27 also shows that the compact version of model checking for L EL -formulas exploiting the notion of α-context is at least as complex as satisfiability checking for L EL -formulas.

Conclusion

We have offered a novel representation of the universal epistemic model which does not require an inductive construction of the agents' belief hierarchies. Our solution exploits the notion of belief base, a natural abstraction for representing epistemic attitudes of rational players in interactive situations, widely used in the area of knowledge representation and reasoning (KR). Our lower bound complexity result for model checking relative to the universal epistemic model clearly displays the trade-off between the compactness of the model checking problem representation and its computational complexity.

Directions of future research are manifold. As emphasized in Section 5, Fagin et al.'s original definition of the universal epistemic model applies to the epistemic logic S5 n which includes principles of positive and negative introspection for knowledge (i.e., if an agent knows that ϕ/does not know that ϕ, then she knows that she knows that ϕ/does not know that ϕ). The logics we presented in this paper do not make any assumption about introspection for belief or knowledge. Future work will be devoted to extend our analysis of the universal epistemic model to variants of epistemic logic with introspection. We also plan to extend our comparative analysis of the different semantics for epistemic logic to more expressive epistemic languages including common belief and distributed belief operators. Last but not least, we plan to explore the connection between the representation of agents' belief hierarchies using the belief base abstraction and type spaces with finite depth of reasoning as defined in [START_REF] Kets | Finite Depth of Reasoning and Equilibrium Play in Games with Incomplete Information[END_REF]. Indeed, the belief base abstraction allows to naturally define the notion of k-level (resource-bounded) reasoner, as an agent whose belief base contains explicit beliefs of at most order k. This is clearly related to the idea of type spaces with finite depth of reasoning à la Kets. where the interpretation of formulas relative to a multi-relational Kripke model M = (W, ⇒ 1 , . . . , ⇒ n , ω) and a world w in W was defined in Section 2. In what follows, for notational convenience we denote elements of W by w, v, u, . . . We define the filtration of M. Let Σ ⊆ L EL be an arbitrary finite set of formulas which is closed under subformulas. (Cf. Definition 2.35 in [START_REF] Blackburn | Modal Logic[END_REF] for a definition of subformulas closed set of formulas.) Let the equivalence relation ≡ Σ on W be defined as follows. For all w, v ∈ W :

w ≡ Σ v iff ∀ϕ ∈ Σ : (M, w) |= ϕ iff (M, v) |= ϕ.
Let |w| Σ be the equivalence class of the world w with respect to the equivalence relation ≡ Σ .

We define W Σ to be the filtrated set of worlds with respect to Σ:

W Σ = {|w| Σ : w ∈ W }.
Clearly, W Σ is a finite set.

Let us define the filtrated valuation function ω Σ . For every p ∈ Atm, we define:

ω Σ (p) = {|w| Σ : (M, w) |= p} if p ∈ Atm(Σ) ω Σ (p) = / 0 otherwise with Atm(Σ) = ψ∈Σ Atm(ψ).
Finally, for every i ∈ Agt, we define agent i's accessibility relation as follows:

⇒ i,Σ = {(|w| Σ , |v| Σ ) : |w| Σ , |v| Σ ∈ W Σ and w ⇒ i v}.
Let us define:

⇒ Σ = i∈Agt ⇒ i,Σ . The model (W Σ , ⇒ 1,Σ , . . . , ⇒ n,Σ , ω Σ ) is the smallest filtration of M under Σ. Let M {ϕ} = (W {ϕ} , ⇒ 1,{ϕ} , . . . , ⇒ n,{ϕ} , ω {ϕ} ). Clearly, we have (M {ϕ} , |w B | {ϕ} ) |= ϕ since (M, w B ) |= ϕ.
In what follows, for notational convenience we denote elements of W {ϕ} by x, y, . . . The next step of the proof consists in unraveling the finite model M {ϕ} up to the modal depth of ϕ. Let We define k-level explicit mutual belief that α in an inductive way as follows:

EB 0 α def = α EB k+1 α def = EB EB k α MB k α def = 0≤h≤k EB h α
where EBα def = i∈Agt i α. We define the labelling function L over nodes in W as follows:

L( - → x ) = p∈Val(ϕ, - → x ) p ∧ p∈Atm(ϕ)\Val(ϕ, - → x ) ¬p ∧ i∈Agt i ⊥ if - → x ∈ Term M L( - → x ) = p∈Val(ϕ, - → x ) p ∧ p∈Atm(ϕ)\Val(ϕ, - → x ) ¬p ∧ i∈Agt i - → y : - → x ⇒ i - → y L( - → y ) if - → x ∈ W \ Term M
where Val(ϕ, -→ x ) = {p ∈ Atm(ϕ) : (M , -→ x ) |= p} is the set of atoms in ϕ which are true at -→ x . Note that every L( -→ x ) is a (finitary) formula of the language L 0 .

The labelling function is used to construct, for every i ∈ Agt, the L 0 -formula which corresponds to the "tree" of valuations rooted in (|w B | {ϕ} ).

Let -→ x 0 = (|w B | {ϕ} ) and let B = (B 1 , . . . , B n , V ) such that:

• for every i ∈ Agt, B i = p∈Atm\Atm(ϕ) {MB depth(ϕ) ¬p} ∪ { - → y ∈W : -→ x 0 ⇒ i -→ y L( -→ y )},

• V = {p : -→ x 0 ∈ ω (p)}.

A.3 Proof of Proposition 23

Proof. The proof is by induction on the structure of the formulas. Boolean cases are trivial. The case ϕ = i ψ is proved in the same way as [START_REF] Fagin | A Model-Theoretic Analysis of Knowledge[END_REF]Lemma 2.5]. Let us prove the case ϕ = ∇ i ψ. Assume that k ≥ h = depth(ϕ) and ( f 0 , . . . , f k ) |= ∇ i ψ. Since ϕ = i ψ, we have h ≥ 1. Moreover, let (g 0 , . . . , g h-1 ) ∈ Z h-1 such that f h (i)(g 0 , . . . , g h-1 ) = 0. By Definition 21, for all (g 0 , . . . , g k-1 ) ∈ Z k-1 , we have f k (i)(g 0 , . . . , g k-1 ) =

Definition 5 (

 5 Multi-agent belief model). A multi-agent belief model (MBM) is a pair (B, Cxt), where B ∈ B and Cxt ⊆ B. The class of MBMs is denoted by M.

Figure 1 :

 1 Figure 1: Conceptual framework

Proposition 8 .

 8 Let (B, Cxt) ∈ M. Then, (B, Cxt) satisfies BC if and only if B ∈ Cxt and B ∈ CB for all B ∈ Cxt.

Theorem 13 .

 13 Let ϕ ∈ L EL . Then, • |= M ϕ if and only if |= B ϕ, • |= M BC ϕ if and only if |= CB ϕ. The following theorem is a corollary of Theorems 10 and 13. Theorem 14. Let ϕ ∈ L EL . Then, • |= B ϕ if and only if |= KripkeM ϕ, • |= CB ϕ if and only if |= ReflKripkeM ϕ.

Proposition 16 .

 16 Let ϕ ∈ L EL , let i ∈ Agt and let (B, B ) (resp. (B, CB )) be a MBM with maximal general uncertainty (resp. a MBM with maximal general uncertainty and belief correctness). Then, • ϕ is satisfiable for the class M if and only if (B, B ) |= ♦ i ϕ, • ϕ is satisfiable for the class M BC if and only if (B, CB ) |= ♦ i ϕ.

=

  Furthermore, it is easy to find a formula χ such that |= M χ and |= B χ. The following formula is an example: ¬U¬ψ and finite X,Y ⊆ Atm such that X ∩Y = / 0. Note that, we can easily adapt the proof of Theorem 10 to show that the set of L EEL -validities relative to the class of multi-relational Kripke models and the set of validities relative to the generic belief base semantics are the same. Theorem 19. Let ϕ ∈ L EEL . Then, • |= M ϕ if and only if |= KripkeM ϕ, • |= M BC ϕ if and only if |= ReflKripkeM ϕ.

  4. Clearly, we have (M, w B ) |= ϕ iff (B, Cxt) |= ϕ. Thus, we have (M, w B ) |= ϕ since (B, Cxt) |= ϕ.

  Seq(ϕ) = {(x 0 , . . . , x k ) : k ≤ depth(ϕ) and x 0 , . . . , x k ∈ W {ϕ} } be the set of sequences of worlds in W {ϕ} of length at most depth(ϕ). Elements of Seq(ϕ) are denoted by -→ x , -→ y , . . . The length of the sequence -→ x is denoted by length( -→ x ). For every 0≤ k ≤ length( -→ x ), -→ x [k] denotes the k-th element in -→ x while -→ x [last] denotes the last element in -→ x . Let -→ x = (x 0 , . . . , x k ), wewrite -→ x .y to denote the sequence (x 0 , . . . , x k , y).We define the tree-like multi-relational Kripke model M = (W , ⇒ 1 , . . . , ⇒ n , ω ) as follows:• W = { -→ x ∈ Seq(ϕ) : -→ x [0] = |w B | {ϕ} and ∀0 ≤ k < length( -→ x ), -→ x [k] ⇒ {ϕ} -→ x [k + 1]},• for every i ∈ Agt and for every -→ x , -→ y ∈ W , -→ x ⇒ i -→ y iff ∃y ∈ W {ϕ} such that -→ y = -→ x .y and -→ x [last] ⇒ i,{ϕ} y, • for every p ∈ Atm, ω (p) = { -→ x ∈ W : -→ x [last] ∈ ω {ϕ} (p)}.Clearly, the tree-like model M is finite. By induction on the structure of ϕ, it is routine exercise to check that (M , -→ x 0 ) |= ϕ iff (M {ϕ} , |w B | {ϕ} ) |= ϕ, with -→ x 0 = (|w B | {ϕ} ). Thus, (M , -→ x 0 ) |= ϕ since (M {ϕ} , |w B | {ϕ} ) |= ϕ.Now, let us denote by Term M the set of terminal nodes in the tree M . That is, Term M = { -→ x ∈ W :∃ -→ y ∈ W such that -→ x ⇒ -→ y } with ⇒ = i∈Agt ⇒ i .

Furthermore, let us

  define the (universal) multi-relational Kripke model M = (W , ⇒ 1 , . . . , ⇒ n , ω ) corresponding to the universal context B as follows: (i) W = {w B : B ∈ B }, (ii) for every i ∈ Agt and for every w B , w B ∈ W , w B ⇒ i w B iff B R i B , and (iii) for every p ∈ Atm, ω(p) = {w B ∈ W : B |= p}. By construction of B , we can show that (M , w B ) and (M , -→ x 0 ) with -→ x 0 = (|w B | {ϕ} ) are depth(ϕ)bisimilar [8, Definition 2.30]. Thus, (M , w B ) |= ϕ since (M , -→ x 0 ) |= ϕ. It follows that (B , B ) |= ϕ, since clearly (M , w B ) |= ϕ iff (B , B ) |= ϕ.

We say that B is correct if and only if, for all i ∈ Agt and for all α ∈ L 0 , if α ∈ B i then B |= α. The class of correct MBBs is denoted by CB. The following definition introduces the concept of epistemic alternative.

  Definition 4 (Epistemic alternatives). Let B, B ∈ B. Then, BR i B if and only if, for every α ∈ B i , B |= α, where the satisfaction relation |= follows Definition 2.BR i B means that B is an epistemic alternative for agent i at B. The idea of the previous definition is that B is an epistemic alternative for agent i at B if and only if, B satisfies all facts that agent i explicitly believes at B.

  Definition 22 (Correct world and belief structure). A world ( f 0 , . . . , f k ) with k ≥ 1 satisfies belief correctness if and only if, for every i ∈ Agt, f k (i)( f 0 , . . . , f k-1 ) = 1. The set of coherent worlds satisfying belief correctness (BC) is denoted by CW BC . We say that the belief structure f = ( f 0 , f 1 , . . .) is correct if, for every k ≥ 1, ( f 0 , . . . , f k ) is a correct world. The set of coherent belief structures satisfying belief correctness (BC) is denoted by CBS BC .

An analysis of the relationship between Harsanyi's type spaces and the multi-relational Kripke semantics of epistemic logic can be found in[START_REF] Galeazzi | Epistemic logic meets epistemic game theory: a comparison between multiagent Kripke models and type spaces[END_REF].

Belle & Lakemeyer [3] offer an inductive construction of the universal epistemic model for the multimodal logic K45 n .

[START_REF] Fagin | A Model-Theoretic Analysis of Knowledge[END_REF] Lemma 2.5] only applies to the standard epistemic language with epistemic operators i and without operators ∇ i .

Other compact formulations of the epistemic logic model checking have been proposed in the literature. For instance[START_REF] Lomuscio | MCMAS: an open-source model checker for the verification of multi-agent systems[END_REF] provide a semantics for epistemic logic model checking based on the concept of interpreted system, while the approach by[START_REF] Van Benthem | Symbolic Model Checking for Dynamic Epistemic Logic[END_REF][START_REF] Van Der Hoek | A logic of revelation and concealment[END_REF][START_REF] Charrier | Building Epistemic Logic from Observations and Public Announcements[END_REF] builds on propositional observability.

Acknowledgements

Support from the ANR project CoPains and the ANR-3IA Artificial and Natural Intelligence Toulouse Institute is gratefully acknowledged.

A Proofs

This appendix presents a selection of the proofs of the technical results presented in the paper.

A.1 Proof of Theorem 10

Proof. We only prove the first item. The proof of the second item is similar.

In order to prove the right-to-left direction we show that if ϕ is satisfiable for M then it is satisfiable for the class of multi-relational Kripke models. Let (B, Cxt) ∈ M such that (B, Cxt) |= ϕ. We build the multi-relational Kripke model M = (W, ⇒ 1 , . . . , ⇒ n , ω) corresponding to (B, Cxt) as follows:

• for every i ∈ Agt and for every w B , w B ∈ W , w B ⇒ i w B iff B R i B ,

• for every p ∈ Atm, ω(p) = {w B ∈ W : B |= p}, Clearly, we have (M, w B ) |= ϕ iff (B, Cxt) |= ϕ. Thus, (M, w B ) |= ϕ since we supposed that (B, Cxt) |= ϕ.

As for the left-to-right direction suppose ϕ is satisfiable for the class of multi-relational Kripke models. We know that the multimodal logic K n interpreted relative to multi-relational Kripke models has the finite model property. Consequently, there exists a finite multi-relational Kripke model M = (W, ⇒ 1 , . . . , ⇒ n , ω) and w ∈ W such that (M, w) |= ϕ. Let name : W → Atm \ Atm(ϕ) be an injective function. Such an injection exists since the set W is finite and the the set Atm is assumed to be infinite. We define the context Cxt = {B v : v ∈ W } where, for every v ∈ W and for every i ∈ Agt,

and

A.2 Proof of Theorem 13

Proof. We prove the first item, as the proof of the second item is analogous. Left-to-right direction is obvious. As for the right-to-left direction, we prove that if ϕ is satisfiable relative to the class M, then it is satisfiable relative to the universal context.

Let (B, Cxt) ∈ M such that (B, Cxt) |= ϕ. We build the multi-relational Kripke model M = (W, ⇒ 1 , . . . , ⇒ n , ω) corresponding to (B, Cxt) as follows:

• for every i ∈ Agt and for every w B ,

A.4 Proof of Theorem 26

Proof. We only prove the first item. The second item can be proved in a similar way.

Let ϕ ∈ L EEL . We will prove that ϕ is satisfiable relative to B iff ϕ is satisfiable relative to the class CBS.

We build the multi-relational Kripke model M = (W, R 1 , . . . , R n , R c 1 , . . . , R c n , ω) corresponding to the Atm(ϕ)-restriction of the universal context B as follows:

• W = {B ∈ B : ∀q ∈ Atm \ Atm(ϕ) and ∀k ≥ 0 :

• for all i ∈ Agt and for all

where the k-level mutual belief operator MB k is defined as in the proof of Theorem 13 (Section A.2). In what follows, for notational convenience we denote elements of W by w, v, u, . . . Interpretation of L EELformulas relative to M and to a world w ∈ W is defined as in Section 2.4 for boolean formulas and for formula i ϕ. We add the following clause for the ∇ i -operator:

We leave to the reader the task of checking that ϕ is satisfiable relative to B iff M satisfies ϕ.

Similarly, we build the multi-relational Kripke model M = (W , T 1 , . . . , T n , T c 1 , . . . , T c n , ω ) corresponding to the Atm(ϕ)-restriction of the set of coherent belief structures as follows:

• W = { f ∈ CBS : ∀q ∈ Atm \ Atm(ϕ), f 0 (q) = 0 and if g 0 (q) = 1 then f k (i)(g 0 , . . . , g k-1 ) = 0, ∀k ≥ 0, ∀i ∈ Agt, ∀g ∈ CBS},

• for all i ∈ Agt and for all f , g ∈ W , f

• for all i ∈ Agt and for all f , g ∈ W , f

Interpretation of L EEL -formulas relative to M and to a world f ∈ W is defined as usual. We have the following truth conditions for the operators i and ∇ i :

We leave to the reader the task of checking that ϕ is satisfiable relative to CBS iff M satisfies ϕ.

For every world w ∈ W in the Kripke model M, we build a coherent belief structure f w = ( f w 0 , f w 1 , . . .). We define f w 0 to be the function such that, for every p ∈ Atm, f w 0 (p) = 1 iff w ∈ ω(p). Moreover, suppose f w 0 , . . . , f w k have been defined for each w ∈ W . Then, we define f w k+1 to be the function such that, for every i ∈ Agt, f w k+1 (i) -1 ({1}) = {(g v 0 , . . . , g v k ) : w ⇒ i v} where f w k+1 (i) -1 ({1}) is the inverse image by f w k+1 (i) of the subset {1} of the codomain {0, 1}.

Let us define the mapping τ : w → f w from W to W . The following intermediate proposition will be useful for the rest of the proof.

Let us define:

where

¬p.

Moreover, for every k > 1, let us define:

g 0 (ϕ)∧ j∈Agt j β j,(g 0 ,...,g k-1 ) .

Note that β i,( f 0 , f 1 ) and every β i,( f 0 ,..., f k ) are (finitary) formulas of L 0 .

We define the multi-agent belief base B f = (B f 1 , . . . , B f n , V f ) as follows:

{MB k ¬q},

Clearly, B f belongs to W . Moreover, it is the case that the multi-agent belief base B f i and the belief structure f define the same belief hierarchy. Specifically, we have τ(B f ) = f . By means of Proposition 28, we can show that the relation {(w, f ) ∈ W ×W : τ(w) = f } is a bisimulation between the Kripke models M and M . Therefore, suppose (M, v) |= ϕ. It follows that (M , τ(v)) |= ϕ. Viceversa, suppose (M , f ) |= ϕ. Then, by Proposition 28, there exists v ∈ W such that τ(v) = f . Since v and f are bisimilar, we have (M, v) |= ϕ.

A.5 Proof of Lemma 1

Proof. In order to prove Lemma 1, we first prove the following intermediate result.

Lemma 2. Let V ⊆ Atm and let χ = λ .π be a quantified boolean formula. Moreover, let B

The proof of the lemma is by induction on the length of the formula χ.

Base case Let λ be the empty sequence. Clearly,

Inductive case We prove that the statement is true for sequence λ of length k + 1, if we suppose it is true for sequence λ of length k. Suppose λ has length k + 1. Therefore, we can assume that λ = Qpλ . We assume

Clearly, for all B ∈ B , we have

Furthermore, by the fact that (B , B ) |= 1 p and (B , B ) |= 1 p, we have that:

Therefore, by induction hypothesis and the fact that (B , B ) |= tr(λ .π) for all B ∈ R [[λ ]] (B ), we have: We can now go back to the statement of Lemma 1 and prove it. The proof of the lemma is by induction on the length of the formula λ .

Base case Suppose λ is the empty sequence and V |= π. By construction of B (χ,V) , the latter is equivalent to B (χ,V) |= π. The latter is equivalent to B (χ,V) , B |= π.

Exploiting Belief Bases for Building Rich Epistemic Structures

Inductive case We prove that the statement is true for sequence λ of length k + 1, if we suppose it is true for sequence λ of length k. Suppose λ has length k + 1. Therefore, χ can be written as Qpλ .π. We assume Q = ∃, as the proof for Q = ∀ is analogous.

(⇒) Suppose V |= ∃pλ .π. The latter is equivalent to saying that V ∪ {p} |= λ .π or V \ {p} |= λ .π. By induction hypothesis, the latter implies that B (λ .π,V∪{p}) , B |= tr(λ .π), or

It is easy to check that V∪{p}) , and

Moreover,

Therefore,

The latter is equivalent to B (χ,V) , B |= tr(χ). (V ∪ {p}) ∩ Atm(π) = V ∩ Atm(π) or

Finally, we have:

Thus, by Lemma 2 and the fact that there exists B ∈ R [[λ ]] B (χ,V) such that B , B |= tr(λ .π), we have: V∪{p}) , B |= tr(λ .π), or B (λ .π,V\{p}) , B |= tr(λ .π).

By induction hypothesis, the latter implies that V ∪{p} |= λ .π or V \{p} |= λ .π. The latter is equivalent to V |= ∃pλ .π.


Andrea Maffia
email: andrea.maffia@unipv.it

Simona Mancarella
email: simona.mancarella@studio.unibo.it

Evidence of relational thinking at kindergarten level

Keywords: Kindergarten, Relational Thinking, Number sentence

Taking inspiration from recent literature about algebraic thinking at early grades, we wonder if and how we can prompt and recognize relational thinking at the kindergarten level. Adopting a design-based research approach, we analyze students' answers to a task, both with the aim of developing its potential in prompting relational thinking and the aim of getting clues about how to recognize relational thinking at the kindergarten level. Analyzing students' behavior while facing our task, we find evidence of relational thinking in students aged 5, even if at different stages. The task proves to be effective in stimulating children relational thinking and in making distinguishable their answers.

Introduction

The distinction between instrumental and relational understanding of mathematics has been originally defined as, respectively, knowing just how mathematical procedures work and knowing both the how and the why [START_REF] Skemp | Relational Understanding and Instrumental Understanding[END_REF]. Such definition found application in the field of arithmetic: several researchers paid attention on prompting students in understanding operations' properties standing behind calculation algorithms. A commonly proposed task consists in finding the missing number in an equality between two arithmetical operations like 39 + 52 =  + 55. Usually, it is assumed that relational thinking is shown if students do not resort to calculation of the results on the two sides of the equality, but they find a solution by compensation or other strategies based on operations' properties and numbers decomposition [START_REF] Carpenter | Thinking mathematically: Integrating arithmetic and algebra in elementary school[END_REF][START_REF] Stephens | Investigating some junctures in relational thinking: a study of year 6 and year 7 students from Australia and China[END_REF].

According to [START_REF] Mason | How Early Is Too Early for Thinking Algebraically?[END_REF], "recognizing that 87 + 54 = 84 + 57 without doing any calculation contributes to and is part of algebraic thinking" (p. 343) and it is never too early to let children thinking in this way. He claims that "the use of natural powers which, when expressed in words and symbols is recognizable as algebra, is called upon from birth if not before" (Mason, 2018, p. 347). Such claim is a starting point for us in wondering if and how we can prompt and recognize relational thinking at the kindergarten level. Adopting a design-based research approach, we analyze students' answers to a task, both with the aim of developing its potential in prompting relational thinking and the aim of getting clues about how to recognize relational thinking at the kindergarten level.

Number sentences written with arithmetical symbols could be inaccessible to students aged 5. This same issue was dealt by Steinweg and colleagues (2018) and Lenz (in press). They developed a suitable task to let kindergarten students approach unknowns. In their task, there are two fictitious characters playing with marbles. They both have the same amount of marbles, but some of them are visible and others are inside colored boxes. Boxes of the same color contain the same amount of marbles. The student is asked to understand how many marbles are in the boxes. [START_REF] Steinweg | Making Implicit Algebraic Thinking Explicit: Exploiting National Characteristics of German Approaches[END_REF] observe that many fourth graders show relational thinking while facing this task. However, according to their data, it seems that younger students have difficulties in dealing with it relationally: "While the majority of kindergarten children indicate numerical values, some children in grades 2 and 4 are already able to describe relationships or dependencies" (Lenz, in press). Kindergarten students "neither describe a relation nor display the dependency between the amounts of marbles in the boxes" (Steinweg et al., 2018, p. 19). We modified the task: In our modified version, students know that there are two characters having the same number of marbles. The first character's marbles are completely visible, while part of the marbles of the second character are in a box. Children have to figure out how many marbles are in the box. Differently than the original task, the amount of marbles in the box is fixed. An example of our task is obtainable taking away the red boxes from Figure 1. We analyzed students' behavior in solving this task assuming the perspective described in the following section.

Theoretical framework

When analyzing their data, [START_REF] Steinweg | Making Implicit Algebraic Thinking Explicit: Exploiting National Characteristics of German Approaches[END_REF] consider as evidence of relational thinking those cases in which a student can express verbally a relation between the quantities of marbles in the boxes: according to them, sentence like "In the green box is always one marble more, than in the orange box" (p. 19) can be considered as relational, because there is an explicit connection between the amounts of marbles in the boxes. Those cases in which students just tell the number of marbles that are in a box were interpreted by them as evidence of the fact that children see the amounts as fixed. We are convinced that some of these cases could be applications of relational thinking. We believe that this can be unveiled by analyzing the process that is enacted by the student to find such results. [START_REF] Carpenter | Thinking mathematically: Integrating arithmetic and algebra in elementary school[END_REF] describe four different benchmarks in the interpretation of number sentences containing the equal sign.

 First benchmark: a very first step in interpreting the equal sign is the student's ability to express his/her own interpretation of the equal sign.  Second benchmark is achieved when students accept equivalences that are not in the standard form a+b=c, for instance c=a+b or a+b=c+d.

 Students at third benchmark compare the two sides of the equal signs carrying out the calculations on each side of the equal sign.  Fourth benchmark is achieved when students can compare the sides of the equality without performing calculations. According to the definitions above, this is relational thinking.

We must stress that, in this paper, we are analyzing a task that is not the same that was used by Carpenter and colleagues to describe these benchmarks. Numbers, operations and equality are not expressed symbolically, but by means of boxes, marbles and verbally. Furthermore, our version of the task does not require calculation on both sides of the equality: the number of marbles on the left side is visible. The algebraic structure of our task is a=x+b with known a and b (number of visible marbles) and unknown x (number of marbles in the box).

We reinterpret benchmarks by [START_REF] Carpenter | Thinking mathematically: Integrating arithmetic and algebra in elementary school[END_REF] in the context of our task. According to our interpretation the first benchmark is reached when children can explain that the number of marbles on the two sides must be the same. Literature shows that understanding the property of 'being the same in quantity' is not granted at kindergarten level [START_REF] Sfard | Why cannot children see as the same what grown-ups cannot see as different? -Early numerical thinking revisited[END_REF].

Second benchmark is achieved if students recognize the structure of the equivalence a=x+b. This is not the case if the student gives a as value for x, interpreting the first part of the equivalence as a=x. This is not reached even if the student counts all the marbles, interpreting the equivalence as a+b=x.

Evidence of the reaching this benchmark could be guessing a value for x that is smaller than a.

When the third benchmark is reached, students use counting to determine the value of x. They can count-on starting from b until they reach a, or they count backward from a to b. We can say that a student reaches the second benchmark, but not the third, when s/he tries to guess a number for x but s/he cannot use counting as a checking strategy. Students at the fourth benchmark can find the number of marbles in the box without a counting procedure, but decomposing numbers, hence showing relational thinking. For instance, they can split a marbles in a group of b marbles and consider that the remaining marbles are as much as those in the box.

We analyzed students answers to the task coding them according to the reached benchmark. The aim is that of answering the following research question: Administering the task, which benchmarks can we observe, distinguish and describe at the kindergarten level?

Methods

Kindergarten children may not be aware of what an adult means while saying that two quantities are "the same" [START_REF] Sfard | Why cannot children see as the same what grown-ups cannot see as different? -Early numerical thinking revisited[END_REF]. For this reason, we organized a first session in which the task was implemented with concrete objects. A group of 21 Italian kindergarten students (aged 5) was divided in small groups of four or five. They seated in front of two paper-characters, one of them holding a box (Figure 2a). Plastic balls were used as marbles. A certain quantity of balls was put in front of the character without box (Marco). The interviewer said that the character with the box (Penelope) had the same quantity of marbles. Some of them were onto the box and some of them were inside. Children were asked to say how many marbles were inside the box. After they said a number, they could actually check by opening the box. We will refer to this first session as training session.

In a second session, the students were again divided in groups of four or five. The task was administered showing images on an interactive whiteboard (Figure 2b), so this time they did not have the chance to open the box to check the number of marbles inside it. The interviewer asked them to say how many marbles are in the box. She also interacted with them asking how they figured it out. In this paper, we analyze video-data from this second session, that we call testing session. Both the training and testing sessions were completely video-reordered and fully transcribed. While transcribing, texts were enriched with screenshots from the video when gestures were performed. Students interventions have been coded with the benchmarks described in the previous section. Both authors discussed together to decide on such coding.

Data analysis

Due to the limit of space, we are not able to show here the complete data analysis. We selected some examples of the different benchmarks that we were able to detect and interpret in our data.

The first benchmark is not reached by all children: When asked to explain the situation, few of them are not able to express in words that the two characters must have the same number of marbles. Apparently, they do not understand what is asked to them and they remain in silence or they change the topic. The following is an example in which we consider that the first benchmark is reached:

Interviewer: Do you remember what we did the last time?

Sofia: Because they always took the balls in the same number, so if he… if Marco took seven, Penelope could take seven because they became friends at the end of the story.

Here the interviewer prompts the child to recall the training session. The student uses the expression 'the same number' to refer to the fact that the two characters have the same amount of balls. According to Sofia, the two sets of balls must have the same property of being seven. Similar explanations are found in other children. They never talk about a correspondence between the two sets of marbles; in other words, they never refer to the fact that for each marble of Marco there is one of Penelope. Statements like that by Sofia, with different numbers as example, are common.

Concerning the second benchmark, we have several examples of children who did not achieve it. For instance, the following excerpt reports the discussion of a group while facing the task in the case in which Marco has six marbles and Penelope has just two marbles outside her box.

Interviewer: What is going on there?

  Figure 1 schematizes a possible instance of the task by Steinweg et al. They administered the task to students aged from 5 to 10.

Figure 1 :

 1 Figure 1: Schematization of the task by Steinweg and colleagues (2018)

Figure 2 :

 2 Figure 2: Settings during training session (left side) and testing session (right side)

We are convinced that the task proved to be effective in terms of eliciting students' processes in determining an unknown quantity in a simple number sentence. Taking the perspective of the designers, we can notice that the task is effective both in stimulating children and in making distinguishable their answers. However, there is still a problem in evidencing those cases in which the second benchmark is reached while the third one is not. Modifications to the task could solve this problem. We can also notice that in our data we have interesting examples of kindergarten students' arguments; it seems that the task could be suitable also to solicit argumentation.

Martina:

Penelope has just two balls.

Interviewer: Just two balls? […] Martina:

No, because the others are inside the box.

Interviewer: And where are those two? […] I heard 'outside'. Is it right?

Emma:

The two balls are outside, but the others are inside.

Interviewer: How many are inside?

Asia: Eight! Asia answers to the interviewers' question naming the number eight, that is the total amount of marbles that are shown in the image (two belonging to Penelope and six belonging to Marco). Even if the question is specifically referring to the marbles inside the box, the student is interpreting the equivalence differently than expected. She is not considering the situation in the form 6=x+2 but as if it were 6+2=x. According to our interpretation, the second benchmark is not yet reached. This happens again in the same little group of students when they face the situation of Marco having five balls and Penelope with four balls outside the box. The students suddenly state that they have the same number, so the interviewer invites them to check by counting; they react counting all the marbles that are shown in the figure. We can notice that reaching the first benchmark is necessary to achieve the second one, but it is not enough. This is shown clearly in the following excerpt.

Luca:

They must have the same number.

Interviewer: They must have the same number; Marco has seven and Penelope has three, how many has she got in the box?

Luca: She must have… Emma: Seven balls?

Luca: Seven.

Luca can state that the two character must have the same number of marbles, however he interprets this sentence relating the number of Marco's marbles with those in Penelope's box. Emma and Luca seem to interpret the equivalence 7=x+3 as if it were 7=x, ignoring the role of the '+3', and so they give the number seven as answer. This is like some cases documented by [START_REF] Carpenter | Thinking mathematically: Integrating arithmetic and algebra in elementary school[END_REF], who found children justifying the presence of an additional number after the equal sign with statements like "it is there just to trick you".

In our data, we do not have cases of students who reached the second benchmark but not the third. Indeed, all those who interpreted correctly the equivalence, then used some counting strategy.

Leonardo: If Penelope has two outside…

Ginevra:

The other four are inside the box.

Leonardo:

Because two plus four… Ginevra:

Here she has two [she points the two marbles that are drawn outside the box] so here she has four [she points the box].

Leonardo: Two [he raises two fingers of his right hand] plus four [he raises four fingers of his left hand], how much is it? Count! [he faces Ginevra, Figure 3a] Ginevra: One, two, three, four, five, six.

Giulia: Indeed, they are six.

In this last excerpt, we can see that Leonardo do not determine the sum 4+2 by himself, but he involves his peers in calculating it to check if the result of such operation is the number of marbles owned by Marco. It is not clear how Ginevra determined that the number of marbles in the box is four. One possibility is that she guessed. Indeed, we have evidence of tentative numbers that are put aside after checking that they are not correct.

(a) (b) (c) Sofia: Penelope has got two outside. Like the last time. Marco has got six, so if she has two outside, it could be that she has… that she has two inside. […] Emma:

If there are two balls outside and other two inside it makes four and Marco has six, so it is not the same number.

Apparently, Sofia is trying to guess the number of marbles in the box, she tries with the number two. Emma follows Sofia's reasoning and she confutes it by summing the supposed amount of marbles with the number of visible marbles owned by Penelope. She realizes that the total amount is different than the number of Marco's marbles and so she rejects Sofia's hypothesis. This kind of guessing and testing strategy could appear not sophisticated but, as Mason notices, "Guess & Test is not only good mathematics, but it can develop over time into more sophisticated versions: Try & Improve, in which the guess is modified according to some principle rather than being essentially random" (Mason, 2008, p. 85). It cannot be considered as relational thinking, but it constitutes a preliminary step for it.

Counting as strategy to determine a sum is frequently used to check the correctness of suggested amounts for marbles in the box. Determining the right number of marbles in the box with different processes appears less frequently. The following excerpt shows one of the few examples. The children are facing the task in the case of Marco having seven marbles and Penelope with three marbles outside the box. They are discussing about the number of marbles that are inside Penelope's box.

Leonardo: They aren't four.

Emma: Yes, four! Because there are seven there.

Ginevra:

Look! Here she has three [she moves her finger along the three marbles that are outside the box, Figure 3b]. Look: here he has three [she moves her finger along three of Marco's marbles] and he has four [she points with both hands to the remaining four Marco's marbles, as she were grasping them, Figure 3c]. So here she has three [she repeats the gesture in Figure 3b pointing to marbles that are outside the box] and here [she repeats the 'grasping gesture' on Penelope's box] she has four.

Interpreting Ginevra's gestures, we can notice that she creates a correspondence between Marco's marbles and Penelope's one. She selects three marbles among Marco's one and she isolates them from the remaining four. Then she notices that Penelope's marbles can be divided again in a group of three (that is shown) and a group of four that is inside the box. The correspondence is made evident by the use of the same gesture (moving the finger along the balls) to point to the groups of three, and a different gesture (grasping the balls with both hands) to point the groups of four. Ginevra is decomposing the number 7 has the sum 4+3 and so she finds the amount of marbles in the box making use of such decomposition. We consider this as an evidence of reaching the fourth benchmark.

Discussion and conclusion

Developing suitable task to let kindergarten students think relationally appears as an important objective if we believe that it is never too early to start thinking algebraically [START_REF] Mason | How Early Is Too Early for Thinking Algebraically?[END_REF]. In this paper, we try to develop such kind of task basing our work on that made by others before. We have modified the task proposed by Steinweg, Akinwunmi and Lenz (2018) because we were not convinced by the fact that they could not observe evidence of relational thinking in children at kindergarten level. Mutuating benchmarks by the work by [START_REF] Carpenter | Thinking mathematically: Integrating arithmetic and algebra in elementary school[END_REF], in our data we can observe different levels of interpretation of a number sentence containing an equivalence. In particular, most of students reach the first benchmark, being able to state what they mean while saying that two amounts are the same in number. We noticed that there are children that are not achieving the second benchmark: they interpret the equivalence a=x+b as if it were a+b=x or a=x. Apparently, they reinterpret the equivalence according to schemes that are more familiar to them.

We do not have evidence of students reaching the second benchmark without reaching also the third one. Using counting to add numbers is used to check the correctness of the amount of marbles in the box. It is not clear if they are using a guess and test method [START_REF] Mason | Making use of children's powers to produce algebraic thinking[END_REF], or if there are other mental processes leading students to suppose a number for the unknown marbles in the box. Evidence of the fourth benchmarck are rare, but there are some. Eventually, we can answer to our research question stating that we find distinguishible evidence of all the four benchmarcks.

This result appears in contrast with that by [START_REF] Steinweg | Making Implicit Algebraic Thinking Explicit: Exploiting National Characteristics of German Approaches[END_REF], however we must notice that it is not easy to directly compare their work with ours. Indeed, even if we are both speaking about relational thinking, it is not sure that we are speaking about the same thing. We used the benchmarks by [START_REF] Carpenter | Thinking mathematically: Integrating arithmetic and algebra in elementary school[END_REF] who consider relational thinking equivalent to the fourth benchmark. We interpreted students' utterances, but also their gestures, as evidence of the process enacted to solve the task. Steinweg and colleagues (2018) use just the words as data and so it is possible that they interpreted differently some cases that we would interpret as relational thinking.

We are aware that there are limitations in this study. Our theoretical framework is modified for this situation, adapting it from the original one that was thought for primary school level. This was necessary because we do not have frameworks for relational thinking at kindergarten level. The framework works well here in describing differences between the behaviors, however it should be tested in other contexts.