Emiliano Lorini
email: emiliano.lorini@irit.fr

Fabian Romero

Decision Procedures for Epistemic Logic Exploiting Belief Bases

We provide tableau-based PSPACE satisfiability checking procedures for a family of multi-agent epistemic logics with a semantics defined in terms of belief bases. Such logics distinguish an agent's explicit beliefs, i.e., all facts included in the agent's belief base, from the agent's implicit beliefs, i.e., all facts deducible from the agent's belief base. We provide a simple dynamic extension for one of these logics by propositional assignments performed by agents. A propositional assignment captures a simple form of action that changes not only the environment but also the agents' beliefs depending on how they jointly perceive its execution. After having provided a PSPACE satisfiability checking procedure for this dynamic extension, we show how it can be used in human-robot interaction in which both the human and the robot have higher-order beliefs about the other's beliefs and can modify the environment by acting.

INTRODUCTION

In [START_REF] Lorini | In Praise of Belief Bases: Doing Epistemic Logic Without Possible Worlds[END_REF], a new epistemic logic called LDA (Logic of Doxastic Attitudes) has been introduced. LDA supports reasoning about explicit beliefs and implicit beliefs of multiple agents. The distinction between explicit belief and implicit belief has been widely discussed in the literature on knowledge representation and reasoning. According to [START_REF] Levesque | A logic of implicit and explicit belief[END_REF], "...a sentence is explicitly believed when it is actively held to be true by an agent and implicitly believed when it follows from what is believed" (p.198). In other words, explicit beliefs correspond to an agent's actual beliefs, whereas implicit beliefs correspond to her potential ones. This distinction is also acknowledged by Fagin & Halpern (F&H)'s logic of general awareness (LGA) [START_REF] Fagin | Belief, Awareness, and Limited Reasoning[END_REF]: it defines explicit belief as a formula implicitly believed by an agent and of which the agent is aware. 1The logic LDA accounts for the connection between the concept of explicit belief and the concept of belief base: an agent's belief base, which is not necessarily closed under deduction, includes all facts that are explicitly believed by the agent. Differently from existing Kripke-style semantics for epistemic logic -exploited, among other logics, by F&H's logic of general awareness -in which the notion of doxastic alternative is primitive, in the LDA semantics the notion of doxastic alternative is defined from, and more generally grounded on, the concept of belief base. 2The main motivation behind the logic LDA is to bridge two traditions that have rarely talked to each other up to now. On the one hand, we have epistemic logic: it started in the 60ies with the seminal work of Hintikka [START_REF] Hintikka | Knowledge and Belief[END_REF] on the logics of knowledge and belief, it was extended to the multi-agent setting at the end of 80ies [START_REF] Fagin | Reasoning about Knowledge[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] Benferhat | A practical approach to revising prioritized knowledge bases[END_REF][START_REF] Hansson | Belief Base Dynamics[END_REF][START_REF] Hansson | Theory contraction and base contraction unified[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 so-called "database perspective" to the theory of intention by [START_REF] Shoham | Logical Theories of Intention and the Database Perspective[END_REF] and resource-bounded knowledge and reasoning about strategies [START_REF] Alechina | Verifying existence of resourcebounded coalition uniform strategies[END_REF]. All these approaches defend the idea that right level of abstraction for understanding and modelling cognitive processes and phenomena is the "belief base" level or, more generally, the "cognitive attitude base" level. The latter consists in identifying a cognitive agent with the sets of facts that she believes (belief base), desires (desire base) and intends (intention base) and in studying the interactions between the different bases. 3There is also a practical motivation behind the logic LDA in relation to modeling Theory of Mind (ToM) in human-machine interaction (HMI) applications including social robots [START_REF] Scassellati | Theory of mind for a humanoid robot[END_REF][START_REF] Winfield | Experiments in Artificial Theory of Mind: From Safety to Story-Telling[END_REF][START_REF] Yang | The grand challenges of Science Robotics[END_REF] and intelligent virtual agents (IVAs) [START_REF] Bosse | A recursive BDI-agent model for theory of mind and its applications[END_REF][START_REF] Harbers | Modeling agents with a theory of mind : Theory-theory versus simulation theory[END_REF][START_REF] Peters | Foundations of an agent theory of mind model for conversation initiation in virtual environments[END_REF][START_REF] Pynadath | Are You Thinking What I'm Thinking? An Evaluation of a Simplified Theory of Mind[END_REF]. An essential aspect of ToM is the general capacity of an agent to form higher-order beliefs about beliefs of other agents. Although existing robotic models of ToM take this aspect into consideration (see, e.g., [START_REF] Breazeal | An Embodied Cognition Approach to Mindreading Skills for Socially Intelligent Robots[END_REF][START_REF] Lemaignan | Artificial cognition for social human-robot interaction: an implementation[END_REF][START_REF] Milliez | A framework for endowing an interactive robot with reasoning capabilities about perspective-taking and belief management[END_REF]), they have some limitations. First of all, they only allow to represent higher-order beliefs of depth at most 2, where the depth of a higher-order belief is defined inductively as follows: (i) an agent's belief has depth 1 if and only if its content is an objective formula that does not mention beliefs of others (e.g., an agent i's belief that it is a sunny day); (ii) an agent's belief has depth n if and only it is a belief about a belief of depth n -1 of another agent (e.g., an agent i's belief of depth 2 that another agent j believes that it is a sunny day). Secondly, models of ToM used for robotic implementations do not have a high level of generality that makes them applicable to different scenarios and situations. As shown by [START_REF] Bolander | Seeing is believing: Formalising false-belief tasks in dynamic epistemic logic[END_REF], the standard epistemic logic approach [START_REF] Fagin | Reasoning about Knowledge[END_REF] allows us to overcome these limitations by allowing to represent higher-order belief of any depth and by offering a general framework for formalizing a large variety of interactive situations between artificial robots and human agents. Unfortunately, it does not distinguish between explicit and implicit beliefs. It only allows to represent what a robot believes a human could potentially believe -if she had enough computational resources and time to infer it -, without representing what the robot believes a human actually believes. Another limitation of the standard epistemic logic approach arises when trying to model complex forms of information dynamics in a multi-agent setting. An example of this is the situation in which a certain action or event takes place, some agents in the system perceive it while others do not, some agents perceive that some agents perceive it, some agents perceive that some agents perceive that some agents perceive it, and so on so forth. Such scenarios are typically modeled in the context of dynamic epistemic logic (DEL) [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF] -the dynamic extension of epistemic logic -with the help of so-called action models [START_REF] Baltag | The Logic of Public Announcements, Common Knowledge and Private Suspicions[END_REF]. However, modeling complex information dynamics in DEL comes with a price. In DEL, whenever an agent privately receives a piece of information, the original epistemic model has to be duplicated by creating one copy of the model for the perceiver in which her beliefs have changed and one copy for the non-perceivers in which their beliefs have not changed [START_REF] Gerbrandy | Reasoning about information change[END_REF]. Thus, the original epistemic model grows exponentially in the length of the sequence of private announcements. Furthermore, although extending multiagent epistemic logic by simple notions of state eliminating public announcement or arrow eliminating private announcement does not increase its PSPACE complexity (see, e.g., [START_REF] Bolander | Announcements to Attentive Agents[END_REF][START_REF] Lutz | Complexity and succinctness of public announcement logic[END_REF]), complexity increases if we move into the realm of full DEL, whose satisfiability problem is known to be NEXPTIME-complete [START_REF] Aucher | On the complexity of dynamic epistemic logic[END_REF].

The logic LDA provides a generalization of the standard epistemic approach in which the distinction between explicit and implicit belief can be captured: it allows us to represent both what a robot believes a human is explicitly believing in a given situationwhich is the essential aspect of ToM -and what a robot believes a human can infer from what she explicitly believes. Moreover, differently from standard DEL, LDA can be easily extended to represent rich belief dynamics in a multi-agent setting, with no increase in complexity with respect to the static logic. The interesting aspect of LDA is that it allows us to model belief dynamics as operations modifying the belief bases of some agents. This leads to a 'parsimonious' account of private informative actions that -differently from traditional DEL -does not require to duplicate epistemic models and to make them exponentially larger.

The aim of the present paper is to explore the practical aspect of the logic LDA: we provide a decision procedure for LDA and for a dynamic extension of it, we discuss its potential applicability in human-robot interaction. The paper is organized as follows. In Section 2, we recall the syntax and the semantics of the logics in the LDA family. Then, in Section 3, we present tableau-based PSPACE satiability checking procedures for these logics. In Section 4, we introduce a dynamic extension of LDA, called DLDA, in which a simple form of action based on propositional assignment can be represented. In DLDA, an assignment is performed by an agent and its execution is privately perceived by some agents. In other words, an assignment changes both the environment and the agents' beliefs depending on perceptive situation, that is to say, on whether they perceive its execution, on whether they perceive other agents perceiving its execution, and so on. We show that the satisfiability problem for DLDA remains in PSPACE and we provide a PSPACE decision procedure for DLDA exploiting a polynomial reduction of DLDA satisfiability to LDA satisfiability. Moreover, we instantiate DLDA in a concrete example of human-robot interaction in a dynamic domain in which the human and the robot not only have higher-order beliefs about the beliefs of the other but also can modify the environment by acting. In Section 5, we conclude.

A LOGIC OF EXPLICIT AND IMPLICIT BELIEF

LDA is a logic for reasoning about explicit beliefs and implicit beliefs of multiple agents. Assume a countably infinite set of atomic propositions Atm = {p, q, . . .} and a finite set of agents Agt = {1, . . . , n}.

We define the language of the logic LDA in two steps. We first 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. 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.

Language L LDA (Atm, Agt), extends language L 0 (Atm, Agt) by modal operators of implicit belief and is defined by the following grammar:

φ ::= α | ¬φ | φ 1 ∧ φ 2 | □ i φ
with α ranging over L 0 (Atm, Agt). For simplicity, we write L 0 instead of L 0 (Atm, Agt) and L LDA instead of L LDA (Atm, Agt), when the context is unambiguous. The other Boolean constructions ⊤, ⊥, ∨, → and ↔ are defined from α, ¬ and ∧ in the standard way.

The formula □ i φ has to be read "agent i implicitly (or potentially) believes that φ is true". 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".

Formal semantics

In this section, we present a semantics for the logic LDA in which the notion of doxastic alternative is not primitive but it is defined from the primitive concept of multi-agent belief base.

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

The class of MBBs is denoted by B.

Formulas of the language L 0 are interpreted relative to multiagent belief bases as follows.

B ̸ |= ⊥ B |= p ⇐⇒ p ∈ S B |= ¬α ⇐⇒ B ̸ |= α B |= α 1 ∧ α 2 ⇐⇒ B |= α 1 and B |= α 2 B |= △ i α ⇐⇒ α ∈ B i
The following definition introduces the concept of doxastic alternative. BR i B ′ means that B ′ is a doxastic alternative for agent i at B. The idea of the previous definition is that B ′ is a doxastic alternative for agent i at B if and only if, B ′ satisfies all facts that agent i explicitly believes at B.

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, Cxt) |= α ⇐⇒ B |= α (B, Cxt) |= □ i φ ⇐⇒ ∀B ′ ∈ Cxt : if BR i B ′ then (B ′ , Cxt) |= φ
Figure 1 illustrates the general idea behind the logic LDA, 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.

Note that the previous semantics does not guarantee that an agent's belief base is globally consistent with the agents' common ground, as it might be the case that there is no B ′ ∈ Cxt such that, for all α ∈ B i , B ′ |= α. In the latter case, we have that (B, Cxt) |= □ i ⊥ which means that agent i's belief base at (B, Cxt) is globally inconsistent with the agent's common ground.

The global consistency property for multi-agent belief models is defined as follows.

B ′ ∈ {B} ∪ Cxt, there exists B ′′ ∈ Cxt such that B ′ R i B ′′ .
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, the terms "true belief", "correct belief" and "knowledge" are usually assumed to be synonyms. The following definition introduces belief correctness for multi-agent belief models. Definition 2.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 ′ .
Clearly, belief correctness implies global consistency. 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 cannot be wrong. For every X ⊆ {GC, BC}, we let M X denote the class of models satisfying all properties in X . Clearly, M ∅ = M. Let φ ∈ L, we say that φ is valid for the class M X , denoted by |= X φ, if and only if, for every (B, Cxt) ∈ M X , we have (B, Cxt) |= φ. For notational convenience, we write |= φ instead of |= ∅ φ. We say that φ is satisfiable for the class M X if and only if ¬φ is not valid for the class M X .

The following definition specifies the conditions under which a rule is applicable. Definition 3.2 (Applicable rule and saturated set). A tableau rule is applicable to a set Γ if Γ is an instance of its numerator and Γ is not an instance of one of its denominators. We say that a set Γ is saturated if there is no rule applicable to it.

The condition requiring that for a tableau rule to be applicable to a set Γ, Γ does not have to be an instance of one of its denominators, guarantees that when constructing a tableau we do not loop indefinitely by applying the same rule infinitely many times.

In the following definition, we introduce the static rules for our tableau method. Definition 3.3 (Static rules). Let X be a finite set of formulas from L LDA , then:

ψ ; ¬ψ ; X ⊥-rule: ⊥ ψ ∧ φ; X ∧-rule: ψ ; φ;ψ ∧ φ; X ¬¬ψ ; X ¬-rule: ψ ; ¬¬ψ ; X △ i α; X △ i -rule: □ i α; △ i α; X ¬(ψ ∧ φ); X ∨-rule: ¬ψ ; ¬(ψ ∧ φ); X | ¬φ; ¬(ψ ∧ φ); X
The following extra rules are used for the KD and KT variants of the logic LDA.

Definition 3.4 (T-rule and D-rule).

Let X be a finite set of formulas from L LDA , then:

□ i ψ ; X T-rule: ψ ; □ i ψ ; X □ i ψ ; X D-rule: i ψ ; □ i ψ ; X
The D-rule corresponds to the property of global consistency (GC) on multi-agent belief models, while the T-rule corresponds to the property of belief correctness (BC). This correspondence is captured by the function cf such that:

cf (D-rule) = GC cf (T-rule) = BC
The transitional rule allows to generate a new successor for a certain agent i. Definition 3.5 (Transitional rule). Let X be a finite set of formulas from L LDA , then:

i ψ ; X i : ψ ; {φ| □ i φ ∈ X }
The following definition introduces the concept of tableau. Definition 3.6 (Tableau). Let X ⊆ {T-rule, D-rule}. A LDA Xtableau for Γ is a tree such that each vertex v carries a pair (Γ ′ , ρ), where Γ ′ is a set of formulas and ρ is one of the following: (i) an instance of a static rule applicable to Γ ′ , (ii) an instance of a rule from X applicable to Γ ′ , (iii) a transitional rule applicable to Γ ′ or iv) the empty rule nihil. The root of the tableau carries a pair (Γ, ρ) for some tableau rule ρ. Moreover, for every vertex v, if v carries the pair (Γ ′ , ρ), then the following conditions hold:

• if Γ ′ is not saturated then ρ nihil, and

• if ρ has k denominators Γ 1 , . . . , Γ k then v has exactly k chil- dren v 1 , . . . , v k such that, for every 1 ≤ h ≤ k, v h carries (Γ h , ρ ′ ) for some tableau rule ρ ′ .
The following definition introduces the concept of closed tableau.

Definition 3.7 (Closed tableau). A branch in a tableau is a path from the root of the tableau to an end vertex, where an end vertex is a vertex carrying a pair (Γ ′ , nihil). A branch in a tableau is closed if its end node is of the form ({⊥}, nihil). A tableau is closed if all its branches are closed, otherwise it is open.

The following theorem highlights that our tableau method is sound. Theorem 3.8. Let φ ∈ L LDA and let X ⊆ {T-rule, D-rule}. Then, if φ is satisfiable for the class M {cf (x ):x ∈X } then all LDA X -tableaux for {φ} are open.

Proof. By means of the truth conditions given in Definitions 2.2 and 2.5, it is straightforward to show that every static rule, every transitional rule and every rule in X applied to a M {cf (x ):x ∈X }satisfiable set of formulas Γ generates some M {cf (x ):x ∈X } -satisfiable set of formulas, where a set of formulas

Γ is M {cf (x ):x ∈X } -satisfiable iff there exists (B, Cxt) ∈ M {cf (x ):x ∈X } such that (B, Cxt) |= φ for all φ ∈ Γ. More precisely, if Γ is M {cf (x ):
x ∈X } -satisfiable and rule ρ is applicable to Γ, then there exists a possible result Γ ′ of applying ρ to Γ such that Γ ′ is M {cf (x ):x ∈X } -satisfiable. 4Thanks to the previous property, by induction on the height of the tableau, it is easy to show that if Γ is M {cf (x ):x ∈X } -satisfiable and Θ is any LDA X -tableau for Γ with finite height then Θ is open.

(Base case). Suppose Θ is a LDA X -tableau for Γ with height 0. Then, (Γ, nihil). Since Γ is M {cf (x ):x ∈X } -satisfiable, Γ {⊤}. Hence, Θ is open.

(Induction case). Suppose Θ is a LDA X -tableau for Γ with height k + 1. By the previous property and the fact that Γ is M {cf (x ):x ∈X }satisfiable, there exists a vertex v such that v is a child of Θ's root, v is the root of a sub-tableau Θ ′ of Θ with height equal or less than k and v carries a pair (Γ ′ , ρ), where Γ ′ is M {cf (x ):x ∈X } -satisfiable.

By induction hypothesis, the sub-tableau Θ ′ is open. Consequently, the tableau Θ is open too.

Since every LDA X -tableau for {φ} has finite height, it follows that if φ is M {cf (x ):x ∈X } -satisfiable then all tableaux for {φ} are open. □

In the rest of this section, we are going to prove that our tableaubased method is complete. Our proof exploits the proof theory of LDA provided in [START_REF] Lorini | In Praise of Belief Bases: Doing Epistemic Logic Without Possible Worlds[END_REF]. In particular, in [START_REF] Lorini | In Praise of Belief Bases: Doing Epistemic Logic Without Possible Worlds[END_REF], it is shown that the logic LDA {D □i } , i.e., the KD variant of the logic LDA, defined by all tautologies of propositional calculus together with the following axioms and rules of inference is sound and complete relative to the class M {GC } :

(□ i φ ∧ □ i (φ → ψ )) → □ i ψ (K □ i ) ¬(□ i φ ∧ □ i ¬φ) (D □ i ) △ i α → □ i α (Int △ i ,□ i ) φ, φ → ψ ψ (MP) φ □ i φ (Nec □ i ) Let □ i φ → φ (T □ i )
Then, it is easy to generalize the completeness proof given in [START_REF] Lorini | In Praise of Belief Bases: Doing Epistemic Logic Without Possible Worlds[END_REF] to show that, for every X ⊆ {D □ i , T □ i }, the logic LDA X is sound and complete for the class M {д(x ):x ∈X } with д(D □ i ) = GC and д(T □ i ) = BC, and where LDA X is the logic defined by all tautologies of propositional calculus, the previous principles

K □ i , Int △ i ,□ i , MP, Nec □ i ,
and all principles in X . Furthermore, it is easy to show that alternative sound and complete axiomatizations for these logics consist in replacing Axiom K □ i and the rule of inference Nec □ i by the following rule of inference:

φ → (ψ 1 ∨ . . . ∨ ψ m ) i φ → ( i ψ 1 ∨ . . . ∨ i ψ m ) (Trans □ i )
Indeed, the rule Trans □ i preserves validity. Moreover, Axiom K □ i and the rule Nec □ i are derivable from it. Therefore, for every X ⊆ {D □ i , T □ i }, we have that if |= {д(x ):x ∈X } φ then ⊢ LDA X φ, where ⊢ LDA X φ, means that there is a proof of φ in LDA X , that is, there is a sequence of formulas (φ 1 , . . . , φ n ) such that:

• φ n = φ,

• for every 1 ≤ k ≤ n, either φ k is an instance of one of the axiom schema of LDA X or there are formulas φ k 1 , . . . , φ k m such that k 1 , . . . , k m < k and

φ k 1 , ...,φ km φ k is an instance of some inference rule of LDA X .
In what follows, we are going to prove that if ⊢ LDA X φ then there exists a LDA X -tableau for {¬φ} which is closed. Before entering into the proof, let us define the collection of all LDA X tableauconsistent sets of formulas. Definition 3.9 (Tableau-consistent sets of formulas). Let X ⊆ {D □ i , T □ i }. We define TC LDA X to be the largest collection of sets of formulas from the language L LDA which satisfies the following conditions. For every Γ ∈ TC LDA X :

• Γ does not contain ⊥, • if Γ ∈ TC LDA X and φ, ¬φ ∈ Γ then Γ ∪ {⊥} ∈ TC LDA X , • if Γ ∈ TC LDA X and φ ∧ ψ ∈ Γ then Γ ∪ {φ,ψ } ∈ TC LDA X , • if Γ ∈ TC LDA X and ¬¬φ ∈ Γ then Γ ∪ {φ} ∈ TC LDA X , • if Γ ∈ TC LDA X and φ ∈ Γ then {¬φ} ∪ Γ TC LDA X , • if Γ ∈ TC LDA X and ¬(φ ∧ ψ ) ∈ Γ then Γ ∪ {¬φ} ∈ TC LDA X or Γ ∪ {¬ψ } ∈ TC LDA X , • if Γ ∈ TC LDA X and △ i α ∈ Γ then Γ ∪ {□ i α } ∈ TC LDA X , • if Γ ∈ TC LDA X and i φ ∈ Γ then {φ} ∪ {ψ : □ i ψ ∈ Γ} ∈ TC LDA X , • if D □ i ∈ X , Γ ∈ TC LDA X and □ i φ ∈ Γ then Γ ∪ { i φ} ∈
TC LDA X , and

• if T □ i ∈ X , Γ ∈ TC LDA X and □ i φ ∈ Γ then Γ ∪ {φ} ∈ TC LDA X .
As the following proposition highlights, tableau consistency is closed under subset operation. Proposition 3.10.

Let X ⊆ {D □ i , T □ i } and let Γ, Γ ′ ⊆ L LDA . Then, if Γ ′ ⊆ Γ and Γ ∈ TC LDA X then Γ ′ ∈ TC LDA X .
Proof. The right-to-left direction is trivial. The left-to-right direction is provable by checking that if Γ ′ ⊆ Γ and Γ ∈ TC LDA X then Γ ′ satisfies all previous conditions for the elements in TC LDA X . □

The following lemma is essential for proving our main result.

Lemma 3.11.

Let X ⊆ {D □ i , T □ i }. Then, if ⊢ LDA X φ then {¬φ} TC LDA X .
Proof. Suppose ⊢ LDA X φ. This means that that there exists a proof of φ in LDA X . By induction on the length of the proof, we show that {¬φ} TC LDA X .

(Base case). Suppose the proof has length 1. This means that φ is an instance of an axiom of the logic LDA X . Suppose φ is an instance of Axiom

Int △ i ,□ i of the form ¬△ i α ∨ □ i α. More- over, suppose that {△ i α ∧ ¬□ i α } ∈ TC LDA X . By definition of TC LDA X , we have {△ i α, ¬□ i α, △ i α ∧ ¬□ i α } ∈ TC LDA X . More- over, {△ i α, □ i α, ¬□ i α, △ i α ∧ ¬□ i α } ∈ TC LDA X and, consequently, {⊥, △ i α, □ i α, ¬□ i α, △ i α ∧¬□ i α } ∈ TC LDA X .
The latter contradicts the fact that every element of TC LDA X does not contain ⊥. We can also prove that if φ is an instance of a tautology of propositional calculus. Moreover, in a similar way, we can prove that if φ an instance of Axiom T □ i (resp. D □ i ) and T □ i ∈ X (resp. D □ i ∈ X ) then {¬φ} TC LDA X .

(Induction case). Suppose the proof has length k + 1. Thus, we have φ = φ k +1 , where φ k +1 is the last element of the proof (φ 1 , . . . , φ k +1 ). Moreover, either φ k +1 is an instance of one of the axiom schema of LDA X , or there are formulas φ k 1 , . . . , φ k m such that k 1 , . . . , k m < k + 1 and

φ k 1 , ...,φ km φ k +1
is an instance of the inference rule Trans □ i . The first case is treated as in the base case of the main proof. Let us prove the second case after assuming that {¬φ k +1 } ∈ TC LDA X . We have that φ k+1 is of the form

i ψ → ( i ψ 1 ∨ . . . ∨ i ψ m ) since φ k +1 is the result of the ap- plication of the inference rule Trans □ i on φ k +1 . Thus, ¬φ k +1 is i ψ ∧ (□ i ¬ψ 1 ∧ . . . ∧ □ i ¬ψ m ). Hence, by definition of TC LDA X , { i ψ ∧□ i ¬ψ 1 ∧ . . . ∧□ i ¬ψ m , i ψ , □ i ¬ψ 1 , . . . , □ i ¬ψ m } ∈ TC LDA X .
Thus, by the definition of TC LDA X , {ψ , ¬ψ 1 , . . . , ¬ψ m } ∈ TC LDA X and, consequently, {ψ , ¬ψ 1 , . . . , ¬ψ m ,ψ ∧ ¬ψ 1 ∧ . . . ∧ ¬ψ m } ∈ TC LDA X . By Proposition 3.10, the latter implies {ψ ∧ ¬ψ 1 ∧ . . . ∧ ¬ψ m } ∈ TC LDA X . Notice that φ k = ψ ∧ ¬ψ 1 ∧ . . . ∧ ¬ψ m . Hence, by induction hypothesis, {ψ ∧ ¬ψ 1 ∧ . . . ∧ ¬ψ m } TC LDA X which leads to a contradiction. □

It is easy to adapt the proof of [START_REF] Fitting | Proof Methods for Modal and Intuitionistic Logics[END_REF]Theorem 6.1] to check that, for every X ⊆ {D □ i , T □ i }, if {¬φ} TC LDA X then there exists a LDA X tableau for {¬φ} which is closed. Thus, by Lemma 3.11 and the completeness of each logic LDA X with respect to its corresponding class of models M {д(x ):x ∈X } , we can state the following theorem. Theorem 3.12. Let φ ∈ L LDA and let X ⊆ {T-rule, D-rule}. Then, if all LDA X -tableaux for {φ} are open then φ is satisfiable for the class M {cf (x ):x ∈X } .

The previous Theorems 3.8 and 3.12 allow us to determine whether a formula φ is satisfiable for the class M {cf (x ):x ∈X } by checking whether all LDA X -tableaux for {φ} are open. Now, following [START_REF] Halpern | A Guide to Completeness and Complexity for Modal Logics of Knowledge and Belief[END_REF], we can easily construct a satisfability checking procedure running in PSPACE based on this result.

To search for the existence of a closed LDA X -tableau for {φ}, we use a backtracking procedure that will construct a closed LDA Xtableau for {φ} if there is any.

The length of a branch of a LDA X -tableau whose root vertex carryies a pair ({¬φ}, ρ), for some arbitrary rule ρ, is polynomial in the size of φ. Since the backtracking procedure only needs to keep in memory a single branch, the procedure runs in PSPACE.

We conclude this section by the following complexity result.

Theorem 3.13. Let X ⊆ {GC, BC}. Then, checking satisfiability of formulas in L LDA relative to the class M X is a PSPACE-complete problem.

Proof. PSPACE-membership is guaranteed to hold by the previous tableau-based satisfiability checking procedure. PSPACEhardness follows from known PSPACE-hardness results for modal logics K, KT and KD [START_REF] Halpern | A Guide to Completeness and Complexity for Modal Logics of Knowledge and Belief[END_REF]. □

DYNAMIC EXTENSION

In this section, we provide a dynamic extension of the logic LDA by a simple form of action of type 'assignment' which consists in setting to true or to false the truth value of a given propositional variable. We call this extension DLDA, which stands for Dynamic LDA. The notion of action viewed as a propositional assignment has been explored by [START_REF] Balbiani | Dynamic Logic of Propositional Assignments: A Well-Behaved Variant of PDL[END_REF][START_REF] Herzig | A Dynamic Logic of Normative Systems[END_REF][START_REF] Tiomkin | Propositional dynamic logic with local assignments[END_REF][START_REF] Van Benthem | Logics of communication and change[END_REF]. It is compatible with the idea of viewing an action as bringing about or effecting (at will) of a change [START_REF] Von | Norm and Action[END_REF].

In DLDA assignments are performed by agents. An assignment changes not only the environment but also the agents' beliefs depending on whether and how they jointly perceive its execution. We call perceptive context a description of what the agents can see in a given situation of interaction. We define it formally as a finite set of formulas from the following language L OBS : ω ::= s i, j | s i ω where i and j range over Agt. The expression s i, j describes the fact that "agent i observes agent j" or, more precisely, "agent i sees what agent j does". The more complex expressions of the form s i ω represents the fact that "agent i sees that ω". For example, s i s z, j represents the fact that "agent i sees that agent z sees what agent j does".

Definition 4.1 (Perception precondition). Let ∆ = j ∈Agt {△ j }, let Seq(∆) be the set of all sequences of elements of ∆ and let i, j ∈ Agt. Elements of Seq(∆) are denoted by σ , σ ′ , . . . We define

F j,i (σ ) = σ ′ ⊑σ { f j,i (σ ′ )}
where f j,i : Seq(∆) -→ L OBS such that:

f j,i (⋏) =s j,i
and for all z ∈ Agt:

f j,i (△ z σ ) =s j f z,i (σ )
with ⋏ the empty sequence and σ ′ ⊑ σ meaning that σ ′ is a subsequence of σ .

F j,i (σ ) identifies the perception precondition for agent j to acquire σ -type information from agent i's performing an action, where ⋏-type information is information about the state of the world and △ z σ -type information is information about agent z's acquiring σ -type information. For example, if σ = △ z then F j,i (σ ) = {s j,i , s j s z,i }. This means that, for agent j to acquire information about z's acquiring information from agent i performing an action, it has to be the case that j sees what i does and j sees that z sees what i does.

The language of the logic DLDA, denoted by L DLDA , is defined by the following grammar:

φ ::= α | ¬φ | φ 1 ∧ φ 2 | □ i φ | [(i,τp,Ω)]φ
where p ranges over Atm, i ranges over Agt, α ranges over the language L 0 defined in Section 2, τ ranges over {+, -} and Ω is a finite set of formulas from the previous language L OBS . The action +p consists in setting the value of the atomic variable p to true, whereas the action -p consists in setting the value of the atomic variable p to false. The formula [(i,τp,Ω)]φ has to be read "φ holds after the performance of the action τp by agent i in the perceptive context Ω". For example, suppose Ω = {s i,i , s j,i , s i s j,i }.

Then, [(i, + p,Ω)]φ means that "φ holds after agent i has set the value of p to true, in the situation in which agent i sees what she does, j sees what i does and i sees that j sees what i does".

The following definition extends the satisfaction relation to the dynamic operator [(i,τp,Ω)].

(B, Cxt) |= [(i,τp,Ω)]φ ⇐⇒ (B (i,τ p, Ω) , Cxt) |= φ with B (i,τ p, Ω) = (B (i,τ p, Ω) 1 , . . . , B (i,τ p, Ω) n
, S (i,τ p, Ω) ), where:

S (i,τ p, Ω) =S ∪ {p} if τ = + S (i,τ p, Ω) =S \ {p} if τ = -
and for all j ∈ Agt:

B (i,τ p, Ω) j = B j ∪ {σp : σ ∈ Seq(∆) and F j,i (σ ) ⊆ Ω} if τ = + B (i,τ p, Ω) j = B j ∪ {σ ¬p : σ ∈ Seq(∆) and F j,i (σ ) ⊆ Ω} if τ = -
where F j,i (σ ) is defined as in Definition 4.1.

According to the previous definition, the effects of the action +p (resp. -p) performed by i in the perceptive context Ω consist in setting the truth value of p to true (resp. false) and in modifying the belief bases of the agents who perceived the action occurrence, according to the perceptive context Ω. The idea is that the performance of action τp by agent i as well as its effects are perceived by agent j if and only if i does τp and j sees what i does (i.e., {s j,i } ⊆ Ω). Agent j believes that the performance of the action τp by i as well as its effects are perceived by agent z 1 if and only if i does τp, j sees what i does, and j sees that z 1 sees what i does (i.e., {s j,i , s j s z 1 ,i } ⊆ Ω). Agent j believes that agent z 1 believes that the performance of the action τp by i as well as its effects are perceived by agent z 2 if and only if i does τp, j sees what i does, j sees that z 1 sees what i does, and j sees that z 1 sees that z 2 sees what i does (i.e., {s j,i , s j s z 1 ,i , s j s z 1 s z 2 ,i } ⊆ Ω), and so on so forth. Note that the execution of an action by an agent does not change the agents' common ground. Dynamics of the agents' common ground under public announcements in the sense of [START_REF] Plaza | Logics of public communications[END_REF] are not investigated in this paper.

The following validities capture some interesting properties of action observation. For all i, j, z ∈ Agt and p ∈ Atm, we have:

|= ¬s j,i → (△ j α ↔ [(i,τp,Ω)]△ j α) (1) |= [(i, + p,Ω)]△ j p if {s j,i } ⊆ Ω (2) |= [(i, -p,Ω)]△ j ¬p if {s j,i } ⊆ Ω (3) |= [(i, + p,Ω)](△ j p ∧ △ j △ z p) if {s j,i , s j s z,i } ⊆ Ω (4) |= [(i, -p,Ω)](△ j ¬p ∧ △ j △ z ¬p) if {s j,i , s j s z,i } ⊆ Ω (5) |= [(i, + p,Ω)]△ j σp if F j,i (σ ) ⊆ Ω (6) |= [(i, -p,Ω)]△ j σ ¬p if F j,i (σ ) ⊆ Ω (7)
According to the first validity, if agent j does not observe agent i, then her explicit beliefs are not affected by what i does. According to the second and third validities, if j observes i and i performs action +p (resp. -p), then agent j will explicitly believe that p (resp. ¬p) afterwards. According to the fourth and fifth validities, if j observes i and j explicitly believes that z observes i, then after i has performed action +p (resp. -p), j will explicitly believe that p (resp. ¬p). Moreover, j will explicitly believe that z explicitly believes that p (resp. ¬p). The sixth and seventh validities generalize the other validities to explicit beliefs of any depth.

Reduction axioms and complexity

The following proposition provides reduction principles for the dynamic operators [(i,τp,Ω)]φ.

Proposition 4.3. The following formulas are valid for the class M:

[(i,τp,Ω)]q ↔ ⊤ if p = q and τ = + [(i,τp,Ω)]q ↔ ⊥ if p = q and τ = -[(i,τp,Ω)]q ↔ q if p q

[(i,τp,Ω)]△ j α ↔ △ j α if α {σp : σ ∈ Seq(∆)} [(i,τp,Ω)]△ j σp ↔ ⊤ if F j,i (σ ) ⊆ Ω [(i,τp,Ω)]△ j σp ↔ △ j σp if F j,i (σ ) ⊈ Ω [(i,τp,Ω)]¬φ ↔ ¬[(i,τp,Ω)]φ [(i,τp,Ω)](φ ∧ ψ ) ↔ ([(i,τp,Ω)]φ ∧ [(i,τp,Ω)]ψ ) [(i,τp,Ω)]□ j φ ↔ □ j ( σ p:F j,i (σ )⊆Ω σp → φ)
The equivalences of Proposition 4.3 allow to find for every formula of the language L DLDA an equivalent formula of the language L LDA . Call red the mapping which iteratively applies the equivalences of Proposition 4.3 from the left to the right, starting from one of the innermost modal operators. red pushes the dynamic operators [(i,τp,Ω)] inside the formula, and finally eliminates them when facing an atomic formula. Specifically, the mapping red is inductively defined by: 1.red(p) = p 2.red(△ j α) = △ j red(α) 3.red(¬φ) = ¬red(φ) 4.red(φ ∧ ψ ) = red(φ) ∧ red(ψ ) 5.red(□ j φ) = □ j red(φ) 6.red([(i,τp,Ω)]q) = red(q) if p = q and τ = + 7.red([(i,τp,Ω)]q) = red(¬q) if p = q and τ = -

8.red([(i,τp,Ω)]q) = red(q) if p q 9.red([(i,τp,Ω)]△ j α) = red(△ j α) if α {σp : σ ∈ Seq(∆)} 10.red([(i,τp,Ω)]△ j σp) = ⊤ if F j,i (σ ) ⊆ Ω 11.red([(i,τp,Ω)]△ j σp) = red(△ j σp) if F j,i (σ ) ⊈ Ω 12.red([(i,τp,Ω)]¬φ) = red(¬[(i,τp,Ω)]φ) 13.red [(i,τp,Ω)](φ ∧ ψ ) = red([(i,τp,Ω)]φ ∧ [(i,τp,Ω)]ψ ) 14.red([(i,τp,Ω)]□ j φ) = red □ j ( σ p:F j, i (σ )⊆Ω σp → φ)
We can state the following proposition. The fact that complexity of DLDA satisfiability checking is in PSPACE follows straightforwardly from the upper bound of complexity for LDA satisfiability checking. Indeed, red provides an effective procedure for reducing a formula φ in L DLDA into an equivalent formula red(φ) in L LDA whose size is polynomial in the size of φ. Therefore, in order to verify whether φ is satisfiable for the class M, one just needs to check whether red(φ) is satisfiable for the class M by using the PSPACE tableau-based satisfiability checking procedure for LDA given in Section 3.

As a consequence, we can state the following complexity result.

Theorem 4.5. Checking satisfiability of formulas in L DLDA relative to the class M is a PSPACE-complete problem.

Example

In this section, we use the logic DLDA to formalize a simple scenario of human-robot interaction in a dynamic domain inspired the famous Sally-Anne false belief's task from the psychological literature on Theory of Mind [START_REF] Baron-Cohen | Does the autistic child have a "theory of mind[END_REF].

We assume that Agt = {h, r } where h denotes the human and r denotes the robot. The scenario is depicted in Figure 2. The human and the robot are standing in front of each other on the opposite sides of a table. The robot has two boxes and two balls in front of him: box 1, box 2, a black ball and a grey ball. In the initial situation the black ball is inside box 1 and the grey ball is inside box 2. The human can perfectly observe her actions as well as the robot's actions. Similarly, the robot can perfectly observe its actions as well as the human's actions. Moreover, the robot can see that the human can see its actions and the human can see that the robot can see her actions. Therefore, the perceptive context is described by the following set of formula from the language L OBS :

Ω 1 = {s r,r , s h,h , s r,h , s h,r , s r s h,r , s h s r,h }.

Let the atomic proposition blackIn1 denote the fact that the black ball is inside box 1 and let blackIn2 denote the fact that the black ball is inside box 2. Similarly, let greyIn1 and greyIn2 denote, respectively, the fact that the grey ball is inside box 1 and the fact that the grey ball is inside box 2. We assume that in the initial situation the human does not explicitly believe that the black ball is inside box 1 and the human does not explicitly believe that the black ball is inside box 2, as she cannot see the box's content. Similarly, the human does not explicitly believe that the grey ball is inside box 1 and the human does not explicitly believe that the grey ball is inside box 2. We also assume that the robot does not explicitly believe that the human explicitly believes that the black ball is inside box 1 (resp. box 2) and that the robot does not explicitly believe that the human explicitly believes that the grey ball is inside box 1 (resp. box 2):

Hyp 1 def = ¬△ h blackIn1 ∧ ¬△ h blackIn2 ∧ ¬△ h greyIn1∧ ¬△ h greyIn2 ∧ ¬△ r △ h blackIn1 ∧ ¬△ r △ h blackIn2∧ ¬△ r △ h greyIn1 ∧ ¬△ r △ h greyIn2
Moreover, we assume that the robot explicitly believes that if the human explicitly believes that one ball is inside one box then she explicitly believes that the ball cannot be inside the other box:

Hyp 2 def = △ r (△ h blackIn1 → △ h ¬blackIn2)∧ (△ h blackIn2 → △ h ¬blackIn1)∧ (△ h greyIn1 → △ h ¬greyIn2)∧ (△ h greyIn2 → △ h ¬greyIn1)
We can use the logic DLDA to infer that, in the perceptive context Ω 1 , if the robot moves the black ball from box 1 to box 2 then, after the occurrence of the action, both the human and the robot will explicitly believe that the black ball is inside box 2, the robot will explicitly believe that the human explicitly believes that the black ball is inside box 2, and the robot will implicitly believe that the human explicitly believes that the black ball is outside box 1:

(Hyp1 ∧ Hyp2) → [(r , + blackIn2,Ω 1 )](△ r blackIn2∧

△ h blackIn2∧ △ r △ h blackIn2∧ □ r △ h ¬blackIn1)
Now, suppose the human moves away so that she cannot see anymore what the robot does and the robot knows this. In other words, let us suppose that situation has changed into the following perceptive context Ω 2 in which the robot and the human can see their own actions but cannot see the actions of the other: Ω 2 = {s r,r , s h,h }.

In the new perceptive context Ω 2 , if the robot moves the grey ball from box 2 to box 1 then, after the occurrence of the robot's action, the human will continue to believe that the black ball is inside box 2, without believing that the grey ball is inside box 1. Moreover, the robot still does not believe that the human believes that the grey ball is inside box 1:

(Hyp1 ∧ Hyp2) →[(r , + blackIn2,Ω 1 )]

[(r , + greyIn1,Ω 2 )](△ h blackIn2∧ ¬△ h greyIn1 ∧ ¬△ r △ h greyIn1)

CONCLUSION

We have presented a family of multi-agent epistemic logics whose semantics exploit the concept of belief base and provided PSPACE tableau-based satisfiability checking procedures for them. Our logics distinguish the concept of explicit belief from the concept of implicit belief. We have introduced a dynamic extension based on propositional assignments whose executions can be more or less visible by the agents. The proposed extension allows us to model higher-order forms of perception, e.g., the fact that a first agent j perceives that a second agent z perceives that a third agent i performs a certain action, thereby coming to believe that z believes that a certain result has been obtained by i's action. We have instantiated the logic in a concrete scenario of human-robot interaction and illustrated its expressive power in capturing subtle aspects of Theory of Mind, with special emphasis on reasoning about beliefs of others on the basis of what the others perceive.

As we have shown in Section 4, if agent i executes a propositional assignment +p (resp. -p) and agent j sees what i does, then agent j will expand her belief base by adding p (resp. ¬p) to it. This belief base expansion operation may make agent j's belief base globally inconsistent. This explains why we only considered the satisfiability problem of formulas in L DLDA relative to the generic class M and not to the classes M GC or M BC . In future research, we plan to study a richer variety of dynamic extensions of the logic LDA by different types of consistency-preserving belief base change operations in the style of [START_REF] Hansson | A Textbook of Belief Dynamics: Theory Change and Database Updating[END_REF]. Another direction we intend to explore is the connection between the logic LDA and machine learning. Specifically, we plan to combine the logic LDA with machine learning methods, such as inductive logic programming, in order to acquire information to be added to an agent's belief base through experience. The interesting and novel aspect of our approach is that an agent's belief base may contain not only propositional facts but also a theory of the other agents' minds and, in particular, information about the other agents' explicit beliefs. Learning a theory of mind is a fascinating issue that, we believe, can be adequately modeled in the context of our semantics for epistemic logic exploiting belief bases.

Definition 2 . 2 (

 22 Satisfaction relation). Let B = (B 1 , . . . , B n , S) be a multi-agent belief base. Then, the satisfaction relation |= between states and formulas in L 0 is defined as follows:

Definition 2 . 3 (

 23 Doxastic alternatives). Let B = (B 1 , . . . , B n , S) and B ′ = (B ′ 1 , . . . , B ′ n , S ′ ) be two multi-agent belief bases. Then, BR i B ′ if and only if, for every α ∈ B i , B ′ |= α, where the satisfaction relation |= follows Definition 2.2.

Definition 2 . 4 (

 24 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. The following definition generalizes the definition of the satisfaction relation |= given in Definition 2.1 to the full language L LDA . Its formulas are interpreted with respect to MBMs. (Boolean cases are omitted, as they are defined in the usual way.) Definition 2.5 (Satisfaction relation (cont.)). Let (B, Cxt) ∈ M. Then:

Figure 1 :

 1 Figure 1: Conceptual framework

Proposition 2 . 8 .

 28 Let (B, Cxt) ∈ M. Then, (B, Cxt) satisfies BC if and only if B ∈ Cxt and, for all i ∈ Agt, B ′ ∈ Cxt and α ∈ B i , we have B ′ |= α.

Definition 4 . 2 (

 42 Satisfaction relation (cont.)). Let B = (B 1 , . . . , B n , S) ∈ B and let (B, Cxt) ∈ M. Then:

Proposition 4 . 4 .

 44 Let φ ∈ L DLDA . Then, φ ↔ red(φ) is valid relative to the class M.

Figure 2 :

 2 Figure 2: Balls in the boxes scenario

For the connection between LDA and LGA, see[START_REF] Lorini | In Praise of Belief Bases: Doing Epistemic Logic Without Possible Worlds (Extended Version)[END_REF], in which a polynomial embedding of the former into the latter is provided.Proc. of the 18th International Conference on Autonomous Agents and Multiagent Systems (AAMAS

2019), N. Agmon, M. E. Taylor, E. Elkind, M. Veloso (eds.), May 13-17, 2019, Montreal, Canada. © 2019 International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.

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

This approach has also been used in linguistic work on modal expressions. For instance, according to[START_REF] Kratzer | The Notional Category of Modality[END_REF], conversational common ground can be seen as set of formulas shared by the interlocutors and the set of worlds that are considered possible by the interlocutors are those worlds that satisfy all formulas in the common ground.

TABLEAUXIn this section, we present a tableau method that can be used for satisfiability of formulas of the logic LDA. As we will deal with sets for the rest of this section, if we use a single formula on a set operation, we mean the singleton containing such formula and we alternatively use ";" as the union operator. Definition 3.1 (Tableau Rule). A tableau rule consists of a set Γ above a line called the numerator, and a list of distinct sets Γ 1 , .., Γ n separated by |, called the denominators:

Γ ′ is a possible result of applying some tableau rule to Γ iff there exists a tableau rule ρ such that Γ is its numerator and Γ ′ is one of its denominators.

ACKNOWLEDGMENTS

This work was supported by the PEPS-CNRS project RoToM "Robots with a Theory of Mind: from logical formalization to implementation".


Emiliano Lorini

Reasoning about Cognitive Attitudes in a Qualitative Setting

We present a general logical framework for reasoning about agents' cognitive attitudes of both epistemic type and motivational type. We provide a sound and complete axiomatization for our logic and we show that it allows us to express a variety of relevant concepts for qualitative decision theory including the concepts of knowledge, belief, strong belief, conditional belief, desire, strong desire, comparative desirability and choice.

Introduction

Since the seminal work of Hintikka on epistemic logic [START_REF] Hintikka | Knowledge and belief: an introduction to the logic of the two notions[END_REF], of Von Wright on the logic of preference [START_REF] Von | The logic of preference[END_REF][START_REF] Von | The logic of preference reconsidered[END_REF] and of Cohen & Levesque on the logic of intention [START_REF] Cohen | Intention is choice with commitment[END_REF], many formal logics for reasoning about cognitive attitudes of agents such as knowledge and belief [START_REF] Fagin | Reasoning about Knowledge[END_REF], preference [START_REF] Liu | Reasoning about Preference Dynamics[END_REF][START_REF] Van Benthem | Everything else being equal: A modal logic for ceteris paribus preferences[END_REF], desire [START_REF] Dubois | The strength of desires: a logical approach[END_REF], intention [START_REF] Shoham | Logical Theories of Intention and the Database Perspective[END_REF][START_REF] Icard | Joint Revision of Beliefs and Intention[END_REF] and their combination [START_REF] Ch | A logical approach to the dynamics of commitments[END_REF][START_REF] Wooldridge | Reasoning about rational agents[END_REF] have been proposed. Generally speaking, these logics are nothing but formal models of rational agency relying on the idea that an agent endowed with cognitive attitudes makes decisions on the basis of what she believes and of what she desires or prefers.

The idea of describing rational agents in terms of their epistemic and motivational attitudes is something that these logics share with classical decision theory and game theory. Classical decision theory and game theory provide a quantitative account of individual and strategic decision-making by assuming that agents' beliefs and desires can be respectively modeled by subjective probabilities and utilities. Qualitative approaches to individual and strategic decision-making have been proposed in AI [START_REF] Boutilier | Towards a logic for qualitative decision theory[END_REF][START_REF] Doyle | Background to qualitative decision theory[END_REF] to characterize criteria that a rational agent should adopt for making decisions when she cannot build a probability distribution over the set of possible events and her preference over the set of possible outcomes cannot be expressed by a utility function but only by a qualitative ordering over the outcomes. For example, going beyond expected utility maximization, qualitative criteria such as the maxmin principle (choose the action that will minimize potential loss) and the maxmax principle (choose the action that will maximize potential gain) have been studied and axiomatically characterized [START_REF] Brafman | An axiomatic treatment of three qualitative decision criteria[END_REF][START_REF] Brafman | On the foundations of qualitative decision theory[END_REF].

The aim of this paper is to present a rich logical framework for representing a variety of agents' cognitive attitudes in a multi-agent setting. In agreement with philosophical theories [START_REF] Platts | Ways of meaning[END_REF][START_REF] Searle | Expression and meaning[END_REF][START_REF] Humberstone | Direction of fit[END_REF][START_REF] Lorini | Logics for Games, Emotions and Institutions[END_REF], our logic allows us to distinguish two general categories of cognitive attitudes: epistemic attitudes, including belief and knowledge, and motivational ones, including desires and preferences. Moreover, in agreement with rational choice theory, it allows us to capture a notion of choice which depends on what an agent believes and desires as well as on the decision criterion she adopts.

The paper is organized as follows. In Section 2, we present the semantics and syntax of our logic, called Dynamic Logic of Cognitive Attitudes (DLCA). At the semantic level, it exploits two orderings that capture, respectively, an agent's comparative plausibility and comparative desirability over states. At the syntactic level, it uses program constructs of dynamic logic (sequential composition, non-deterministic choice, intersection, converse and test) to build complex cognitive attitudes from simple ones. Following [START_REF] Passy | An essay in combinatorial dynamic logic[END_REF][START_REF] Gargov | Modal logic with names[END_REF], it also uses nominals in order to axiomatize intersection of programs. In Section 3, we illustrate the expressive power of our logic by using it to formalize a variety of cognitive attitudes of agents including knowledge, belief, strong belief, conditional belief, desire, strong desire, comparative desirability and choice. In Section 4, we present a sound and complete axiomatization for it. In Section 5 we conclude.

Dynamic Logic of Cognitive Attitudes

Let Atm be a countable infinite set of atomic propositions, let Nom be a countable infinite set of nominals disjoint from Atm and let Agt be a finite set of agents.

Definition 1 (Multi-agent cognitive model

). A multi-agent cognitive model (MCM) is a tuple M = (W, ( i,P ) i∈Agt , ( i,D ) i∈Agt , (≡ i ) i∈Agt , V ) where:
-W is a set of worlds or states; for every i ∈ Agt, i,P and i,D are preorders on W and ≡ i is an equivalence relation on W such that for all τ ∈ {P, D} and for all w, v ∈ W :

(C1) i,τ ⊆≡ i , (C2) if w ≡ i v then w i,τ v or v i,τ w; -V : W -→ 2 Atm∪Nom is a valuation function such that for all w, v ∈ W : (C3) V Nom (w) = ∅, (C4) if V Nom (w) ∩ V Nom (v) = ∅ then w = v; where V Nom (w) = Nom ∩ V (w).
w i,P v means that, according to agent i, v is at least as plausible as w, whereas w i,D v means that, according to agent i, v is at least as desirable as w. Finally, w ≡ i v means that w and v are indistinguishable for agent i. For every w ∈ W , ≡ i (w) is also called agent i's information set at state w. According to Constraint C1, an agent can only compare the plausibility (resp. desirability) of two states in her information set. According to Constraint C2, the plausibility (resp. desirability) of two states in an agent's information set are always comparable. Constraints C3 and C4 capture the two basic properties of nominals: every state is associated with at least one nominal and there are no different states associated with the same nominal.

We introduce the following modal language L DLCA (Atm, Nom, Agt), or simply L DLCA , for the Dynamic Logic of Cognitive Attitudes DLCA:

π ::= ≡ i | i,P | i,D | ∼ i,P | ∼ i,D | π;π | π ∪ π | π ∩ π | -π | ϕ? ϕ ::= p | x | ¬ϕ | ϕ ∧ ϕ | [π]ϕ
where p ranges over Atm, x ranges over Nom and i ranges over Agt. The other Boolean constructions , ⊥, ∨, → and ↔ are defined from p, ¬ and ∧ in the standard way.

Elements π are called cognitive programs or, more shortly, programs. The set of all programs is denoted by P(Atm, Nom, Agt), or simply, P.

Cognitive programs correspond to the basic constructions of Propositional Dynamic Logic (PDL) [START_REF] Harel | Dynamic Logic[END_REF]: atomic programs of type ≡ i , i,P , i,D , ∼ i,P and ∼ i,D , sequential composition (;), non-deterministic choice (∪), intersection (∩), converse ( -) and test (?). A given cognitive program π corresponds to a specific configuration of the agents' cognitive states including their epistemic states and their motivational states.

The formula [π]ϕ has to be read "ϕ is true, according to the cognitive program π". As usual, we define π to be the dual operator of

[π], that is, π ϕ = def ¬[π]¬ϕ.
The atomic program ≡ i represents the standard S5, partition-based and fully introspective notion of knowledge [START_REF] Fagin | Reasoning about Knowledge[END_REF][START_REF] Aumann | Interactive epistemology I: Knowledge[END_REF]. [≡ i ]ϕ has to be read "ϕ is true according to what agent i knows" or more simply "agent i knows that ϕ is true", which just means that "ϕ is true in all worlds that agent i envisages".

The atomic programs i,P and i,D capture, respectively, agent i's plausibility ordering and agent i's desirability ordering over facts. In particular, [ i,P ]ϕ has to be read "ϕ is true at all states that, according to agent i, are at least as plausible as the current one", while [ i,D ]ϕ has to be read "ϕ is true at all states that, according to agent i, are at least as desirable as the current one". The atomic programs ∼ i,P and ∼ i,D are the complements of the atomic programs i,P and i,D , respectively. In particular, [ ∼ i,P ]ϕ has to be read "ϕ is true at all states that, according to agent i, are not at least as plausible as the current one", while [ ∼ i,D ]ϕ has to be read "ϕ is true at all states that, according to agent i, are not at least as desirable as the current one". The program constructs ;, ∪, ∩,and ? are used to define complex cognitive programs from the atomic cognitive programs. For example, the formula [ i,P ∪ i,D ]ϕ has to be read "ϕ is true at all states that, according to agent i, are either at least as plausible or at least as desirable as the current one", whereas the formula [ i,P ∩ i,D ]ϕ has to be read "ϕ is true at all states that, according to agent i, are at least as plausible and at least as desirable as the current one".

The following definition provides truth conditions for formulas in L DLCA :

Definition 2 (Truth conditions). Let M = (W, ( i,P ) i∈Agt , ( i,D ) i∈Agt , (≡ i ) i∈Agt , V ) be a MCM and let w ∈ W . Then: M, w |= p ⇐⇒ p ∈ V (w) M, w |= x ⇐⇒ x ∈ V (w) M, w |= ¬ϕ ⇐⇒ M, w |= ϕ M, w |= ϕ ∧ ψ ⇐⇒ M, w |= ϕ and M, w |= ψ M, w |= [π]ϕ ⇐⇒ ∀v ∈ W : if wR π v then M, v |= ϕ
where the binary relation R π on W is inductively defined as follows, with τ ∈ {P, D}:

wR ≡i v iff w ≡ i v wR i,τ v iff w i,τ v wR ∼ i,τ v iff w ≡ i v and w i,τ v wR π;π v iff ∃u ∈ W : wR π u and uR π v wR π∪π v iff wR π v or wR π v wR π∩π v iff wR π v and wR π v wR -π v iff vR π w wR ϕ? v iff w = v and M, w |= ϕ
For notational convenience, we use wR π v and (w, v) ∈ R π as interchangeable notations.

We can build a variety of cognitive programs capturing different types of plausibility and desirability relations between possible worlds. For instance, for every τ ∈ {P, D}, we can define:

i,τ = def -i,τ i,τ = def i,τ ∩ ∼ i,τ ∼ i,τ = def -∼ i,τ ≺ i,τ = def i,τ ∩ ∼ i,τ ≈ i,τ = def i,τ ∩ i,τ
The five definitions denote respectively "at most as plausible (resp. desirable) as", "less plausible (resp. desirable) than", "not at most as plausible (resp. desirable) as", "more plausible (resp. desirable) than" and "equally plausible (resp. desirable) as".

For every formula ϕ in L DLCA we say that ϕ is valid if and only if for every multiagent cognitive model M and world w in M , we have M, w |= ϕ. Conversely, we say that ϕ is satisfiable if ¬ϕ is not valid.

For a given multi-agent cognitive model M = (W, ( i,P ) i∈Agt , ( i,D ) i∈Agt , (≡ i ) i∈Agt , N, V ), we define ||ϕ|| M = {v ∈ W : M, v |= ϕ} to be the truth set of ϕ in M . Moreover, for every w ∈ W and for every i ∈ Agt, we define ||ϕ|| i,w,M = {v ∈ W : M, v |= ϕ and w ≡ i v} to be the truth set of ϕ from i's point of view at state w in M .

Formalization of Cognitive Attitudes

In this section, we show how the logic DLCA can be used to model the variety of cognitive attitudes of agents that we have briefly discussed in Section 1.

Epistemic attitudes

We start with the family of epistemic attitudes by defining a standard notion of belief. We say that an agent believes that ϕ if and only if ϕ is true at all states that the agent considers maximally plausible. Definition 3 (Belief). Let M = (W, ( i,P ) i∈Agt , ( i,D ) i∈Agt , (≡ i ) i∈Agt , V ) be a MCM and let w ∈ W . We say that agent i believes that ϕ at w, denoted by M, w |= B i ϕ, if and only if Best i,P (w) ⊆ ||ϕ|| M where Best i,P (w) = {v ∈ W : w ≡ i v and ∀u ∈ W, if w ≡ i u then u i,P v}.

As the following proposition highlights, the previous notion of belief is expressible in the logic DLCA by means of the cognitive program ≡ i ; [≺ i,P ]⊥?.

Proposition 1. Let M = (W, ( i,P ) i∈Agt , ( i,D ) i∈Agt , (≡ i ) i∈Agt , V ) be a MCM and let w ∈ W . Then, we have M, w |= B i ϕ iff M, w |= ≡ i ; [≺ i,P ]⊥? ϕ.
It is worth noting that the set Best i,P (w) in Definition 3 might be empty, since it is not necessarily the case that the relation i,P is conversely well-founded. 1 As a consequence, the belief operator B i does not necessarily satisfy Axiom D, i.e., the formula B i ϕ ∧ B i ¬ϕ is satisfiable in the logic DLCA. More details about these aspects will be given at the end of Section 4.

In the literature on epistemic logic [START_REF] Baltag | Talking your way into agreement: Belief merge by persuasive communication[END_REF], mere belief of Definition 3 is usually distinguished from strong belief. Specifically, we say that an agent strongly believes that ϕ if and only if, according to agent i, all ϕ-worlds are strictly more plausible than all ¬ϕ-worlds.

Definition 4 (Strong belief). Let M = (W, ( i,P ) i∈Agt , ( i,D ) i∈Agt , (≡ i ) i∈Agt , V )
be a MCM and let w ∈ W . We say that agent i strongly believes that ϕ at w, denoted by M, w |= SB i ϕ, if and only if ∀v ∈ ||ϕ|| i,w,M and ∀u ∈ ||¬ϕ|| i,w,M : u ≺ i,P v.

As the following proposition highlights, the previous notion of strong belief is expressible in the logic DLCA by means of the cognitive program ≡ i ; ϕ?; i,P . Proposition 2. Let M = (W, ( i,P ) i∈Agt , ( i,D ) i∈Agt , (≡ i ) i∈Agt , V ) be a MCM and let w ∈ W . Then, we have

M, w |= SB i ϕ iff M, w |= ≡ i ; ϕ?; i,P ϕ.
Strong belief that ϕ implies belief that ϕ, if the agent envisages at least one state in which ϕ is true. This property is expressed by the following validity:

|= SB i ϕ ∧ ≡ i ϕ → B i ϕ (1)
Conditional belief is another notion which has been studied by epistemic logicians given its important role in belief dynamics [START_REF] Van Benthem | Dynamic logic for belief revision[END_REF]. We say that an agent believes that ϕ conditional on ψ, or she would believe that ϕ if she learnt that ψ, if and only if, according to agent i, all most plausible ψ-worlds are also ϕ-worlds.

Definition 5 (Conditional belief). Let M = (W, ( i,P ) i∈Agt , ( i,D ) i∈Agt , (≡ i ) i∈Agt , V ) be a MCM and let w ∈ W . We say that agent i would believe that ϕ if she learnt that ψ at w, denoted by M, w |= B i (ψ, ϕ), if and only if Best i,P (ψ, w) ⊆ ||ϕ|| M , where Best i,P (ψ, w) = {v ∈ ||ψ|| i,w,M : ∀u ∈ ||ψ|| i,w,M , u i,P v}.

Note that Best i,P ( , w) = Best i,P (w).

As for belief and strong belief, we have a specific cognitive program ≡ i ; (ψ ∧ [≺ i,P ]¬ψ)? corresponding to the belief that ϕ conditional on ψ, so that the latter can be represented in in the language of the logic DLCA. Proposition 3. Let M = (W, ( i,P ) i∈Agt , ( i,D ) i∈Agt , (≡ i ) i∈Agt , V ) be a MCM and let w ∈ W . Then, we have

M, w |= B i (ψ, ϕ) iff M, w |= ≡ i ; (ψ ∧ [≺ i,P ]¬ψ)? ϕ.

Motivational attitudes

The first kind of motivational attitude we consider is desire. Following [START_REF] Dubois | The strength of desires: a logical approach[END_REF], we say that an agent desires that ϕ if and only if all states that the agent envisages at which ϕ is true is true are not minimally desirable for the agent. In other words, desiring that ϕ consists in having some degree of attraction for all situations in which ϕ is true. Definition 6 (Desire). Let M = (W, ( i,P ) i∈Agt , ( i,D ) i∈Agt , (≡ i ) i∈Agt , V ) be a MCM and let w ∈ W . We say that agent i desires that ϕ at w, denoted by M, w

|= D i ϕ, if and only if Worst i,D (w) ∩ ||ϕ|| M = ∅, where Worst i,D (w) = {v ∈ W : w ≡ i v and ∀u ∈ W, if w ≡ i u then v i,D u}.
As the following proposition highlights, the previous notion of desire is characterized by the cognitive program ≡ i ; [ i,D ]⊥?. Proposition 4. Let M = (W, ( i,P ) i∈Agt , ( i,D ) i∈Agt , (≡ i ) i∈Agt , V ) be a MCM and let w ∈ W . Then, we have

M, w |= D i ϕ iff M, w |= ≡ i ; [ i,D ]⊥? ¬ϕ.
Similarly to the set Best i,P (w) in Definition 3, the set Worst i,D (w) in Definition 6 might be empty, since it is not necessarily the case that the relation i,D is wellfounded. 2 As a consequence, desires are not necessarily consistent, i.e., the formula D i ϕ ∧ D i ¬ϕ is satisfiable in the logic DLCA. As emphasized by [START_REF] Dubois | The strength of desires: a logical approach[END_REF], this notion of desire satisfies the following property:

|=D i ϕ → D i (ϕ ∧ ψ) (2)
Indeed, if an agent has some degree of attraction for all situations in which ϕ is true then, clearly, it should have some degree of attraction for all situations in which ϕ ∧ ψ is true, since all ϕ ∧ ψ-situations are also ϕ-situations. It is a property that this notion of desire shares with the open reading of the concept of permission studied in the area of deontic logic (see, e.g., [START_REF] Anglberger | Obligation, free choice, and the logic of weakest permissions[END_REF][START_REF] Lewis | A problem about permission[END_REF]). 3One way of blocking this inference is by strengthening the notion of desire. We say that an agent strongly desires that ϕ if and only if, according to agent i, all ϕ-worlds are strictly more desirable than all ¬ϕ-worlds.

Definition 7 (Strong desire). Let M = (W, ( i,P ) i∈Agt , ( i,D ) i∈Agt , (≡ i ) i∈Agt , V ) be a MCM and let w ∈ W . We say that agent i strongly desires that ϕ at w, denoted by M, w |= SD i ϕ, if and only if ∀v ∈ ||ϕ|| i,w,M and ∀u ∈ ||¬ϕ|| i,w,M : u ≺ i,D v.

As for desire, there exists a cognitive program which characterizes strong desire, namely, the program ≡ i ; ϕ?; i,D . Proposition 5. Let M = (W, ( i,P ) i∈Agt , ( i,D ) i∈Agt , (≡ i ) i∈Agt , V ) be a MCM and let w ∈ W . Then, we have

M, w |= SD i ϕ iff M, w |= ≡ i ; ϕ?; i,D ϕ.
We have that strong desire implies desire:

|=SD i ϕ → D i ϕ (3)
Differently from desiring, it is not necessarily the case that strongly desiring that ϕ implies strongly desiring that ϕ ∧ ψ, i.e., the formula SD i ϕ ∧ ¬SD i (ϕ ∧ ψ) is satisfiable in the logic DLCA. Indeed, strongly desiring that ϕ is compatible with envisaging a situation in which ϕ ∧ ψ holds and another situation in which ϕ ∧ ¬ψ holds such that the first situation is less desirable than the second one.

From comparative desirability to choice

We consider two views about comparative statements between formulas of the form "the state of affairs ϕ is for agent i at least as desirable as the state of affairs ψ". According to the optimistic view, when assessing whether ϕ is at least as desirable as ψ, an agent focuses on the best ϕ-situations in comparison with the best ψ-situations. Specifically, an "optimistic" agent i considers ϕ at least as desirable as ψ if and only if, for every ψ-situation envisaged by i there exists a ϕ-situation envisaged by i such that the latter is at least as desirable as the former. According to the pessimistic view, she focuses on the worst ϕ-situations in comparison with the worst ψ-situations. Specifically, a "pessimistic" agent i considers ϕ at least as desirable as ψ if and only if, for every ϕsituation envisaged by i there exists a ψ-situation envisaged by i such that the former is at least as desirable as the latter.

Let us first define comparative desirability according to the optimistic view.

Definition 8 (Comparative desirability: optimistic view). Let M = (W, ( i,P ) i∈Agt , ( i,D ) i∈Agt , (≡ i ) i∈Agt , V ) be a MCM and let w ∈ W . We say that, according to agent i's optimistic assessment, ϕ is at least as desirable as ψ at w, denoted by M, w |=

D Opt i (ψ ϕ), if and only if ∀u ∈ ||ψ|| i,w,M , ∃v ∈ ||ϕ|| i,w,M : u i,D v.
As the following proposition highlights, it is expressible in the language L DLCA . Proposition 6. Let M = (W, ( i,P ) i∈Agt , ( i,D ) i∈Agt , (≡ i ) i∈Agt , V ) be a MCM and let w ∈ W . Then, we have

M, w |= D Opt i (ψ ϕ) iff M, w |= ≡ i ; ψ? i,D ϕ.
The following abbreviation defines strict comparative desirability according to the optimistic view:

D Opt i (ψ ≺ ϕ) = def D Opt i (ψ ϕ) ∧ ¬D Opt i (ϕ ψ) D Opt i (ψ ≺ ϕ)
has to be read "according to i's optimistic assessment, ϕ is more desirable than ψ".

Let us now define comparative desirability according to the pessimistic view.

Definition 9 (Comparative desirability: pessimistic view). Let M = (W, ( i,P ) i∈Agt , ( i,D ) i∈Agt , (≡ i ) i∈Agt , V ) be a MCM and let w ∈ W . We say that, according to agent i's pessimistic assessment, ϕ is at least as desirable as ψ at w, denoted by

M, w |= D Pess i (ψ ϕ), if and only if ∀v ∈ ||ϕ|| i,w,M , ∃u ∈ ||ψ|| i,w,M : u i,D v.
As for the optimistic view, the pessimistic view is also expressible in the language L DLCA . Proposition 7. Let M = (W, ( i,P ) i∈Agt , ( i,D ) i∈Agt , (≡ i ) i∈Agt , V ) be a MCM and let w ∈ W . Then, we have

M, w |= D Pess i (ψ ϕ) iff M, w |= ≡ i ; ϕ? i,D ψ.
The following abbreviation defines strict comparative desirability according to the pessimistic view:

D Pess i (ψ ≺ ϕ) = def D Pess i (ψ ϕ) ∧ ¬D Pess i (ϕ ψ) D Pess i (ψ ≺ ϕ)
has to be read "according to i's pessimistic assessment, ϕ is more desirable than ψ".

The previous notion of (optimistic and pessimistic) comparative desirability does not depend on what the agent believes. This means that, in order to assess whether ϕ is at least as desirable as ψ, an agent also takes into account worlds that are implausible (or, more generally, not maximally plausible). Realistic comparative desirability requires that an agent compares two formulas ϕ and ψ only with respect to the set of most plausible states. This idea has been discussed in the area of qualitative decision theory by different authors [START_REF] Boutilier | Towards a logic for qualitative decision theory[END_REF][START_REF] Brafman | An axiomatic treatment of three qualitative decision criteria[END_REF][START_REF] Brafman | On the foundations of qualitative decision theory[END_REF].

The following definition introduces realistic comparative desirability according to the optimistic view.

Definition 10 (Realistic comparative desirability: optimistic view). Let M = (W, ( i,P ) i∈Agt , ( i,D ) i∈Agt , (≡ i ) i∈Agt , V ) be a MCM and let w ∈ W . We say that, according to agent i's optimistic assessment, ϕ is realistically at least as desirable as

ψ at w, denoted by M, w |= RD Opt i (ψ ϕ), if and only if ∀u ∈ Best i,P (w) ∩ ||ψ|| i,w,M , ∃v ∈ Best i,P (w) ∩ ||ϕ|| i,w,M : u i,D v.
The idea is that an "optimistic" agent i considers ϕ realistically at least as desirable as ψ if and only if, for every ψ-situation in agent i's belief set there exists a ϕ-situation in agent i's belief set such that the latter is at least as desirable as the former.

The previous notion as well is expressible in the language L DLCA .

Proposition 8. Let M = (W, ( i,P ) i∈Agt , ( i,D ) i∈Agt , (≡ i ) i∈Agt , V ) be a MCM and let w ∈ W . Then, we have

M, w |= RD Opt i (ψ ϕ) iff M, w |= ≡ i ; [≺ i,P ]⊥?; ψ? i,D ∩(≡ i ; [≺ i,P ]⊥?) ϕ.
We define:

RD Opt i (ψ ≺ ϕ) = def RD Opt i (ψ ϕ) ∧ ¬RD Opt i (ϕ ψ)
RD Opt i (ψ ≺ ϕ) has to be read "according to agent i's optimistic assessment, ϕ is realistically more desirable than ψ".

The following definition introduces realistic comparative desirability according to the pessimistic view.

Definition 11 (Realistic comparative desirability: pessimistic view). Let M = (W, ( i,P ) i∈Agt , ( i,D ) i∈Agt , (≡ i ) i∈Agt , V ) be a MCM and let w ∈ W . We say that, according to agent i's pessimistic assessment, ϕ is realistically at least as desirable as

ψ at w, denoted by M, w |= RD Pess i (ψ ϕ), if and only if ∀v ∈ Best i,P (w) ∩ ||ϕ|| i,w,M , ∃u ∈ Best i,P (w) ∩ ||ψ|| i,w,M : u i,D v.
The idea is that a "pessimistic" agent i considers ϕ realistically at least as desirable as ψ if and only if, for every ϕ-situation in agent i's belief set there exists a ψ-situation in agent i's belief set such that the former is at least as desirable as the latter.

It is also expressible in the language L DLCA .

Proposition 9. Let M = (W, ( i,P ) i∈Agt , ( i,D ) i∈Agt , (≡ i ) i∈Agt , V ) be a MCM and let w ∈ W . Then, we have

M, w |= RD Pess i (ψ ϕ) iff M, w |= ≡ i ; [≺ i,P ]⊥?; ϕ? i,D ∩(≡ i ; [≺ i,P ]⊥?) ψ.
We define:

RD Pess i (ψ ≺ ϕ) = def RD Pess i (ψ ϕ) ∧ ¬RD Pess i (ϕ ψ)
RD Pess i (ψ ≺ ϕ) has to be read "according to agent i's pessimistic assessment, ϕ is realistically more desirable than ψ".

We conclude this section by defining two notions of choice: agent i's optimistic choice that ϕ, denoted by C Opt i ϕ, and agent i's pessimistic choice that ϕ, denoted by C Pess i ϕ.

C Opt i ϕ = def RD Opt i (¬ϕ ≺ ϕ) C Pess i ϕ = def RD Pess i (¬ϕ ≺ ϕ)
According to these definitions, an optimistic (resp. pessimistic) agent should choose ϕ if and only if, according to her optimistic (resp. pessimistic) assessment, ϕ is realistically more desirable than ¬ϕ.

We conclude this section by discussing the properties of converse well-foundedness for the relation i,P and well-foundedness for the relation i,D . As emphasized in Section 3, these properties are required to make agents' beliefs and desires consistent, namely, to guarantee that the formulas ¬(B i ϕ ∧ B i ¬ϕ) and ¬(D i ϕ ∧ D i ¬ϕ) become valid. It turns out that these properties can be easily added to our logical framework.

In particular, let us consider the class of multi-agent cognitive models whose relations i,D and i,P are, respectively, well-founded and conversely well-founded.

Furthermore, let us consider the following two axioms:

≡ i ψ → ≡ i (ψ ∧ [≺ i,P ]¬ψ) (CWF i,P ) ≡ i ψ → ≡ i (ψ ∧ [ i,D ]¬ψ) (WF i,D )
Let us define DLCA wf to be the extension of the logic DLCA of Definition 12 by these axioms. It is straightforward to verify that the logic DLCA wf is sound for the class of multi-agent cognitive models whose relations i,D and i,P are, respectively, wellfounded and conversely well-founded. We conjecture that we can easily adapt the proof of Theorem 1 to show that it is also complete.

Conclusion

We have presented a logical framework for modelling a rich variety of cognitive attitudes of both epistemic type and motivational type. We have provided a sound and complete axiomatization for our logic.

Directions of future research are manifold. The present paper is devoted to study the proof-theoretic aspects of the logic. In future work, we plan to investigate its computational aspects including decidability of its satisfiability problem and, at a later stage, complexity. In order to prove decidability, we expect to be able to use existing filtration techniques from modal logic. Following the literature on dynamic epistemic logic (DEL) [START_REF] Van Ditmarsch | Dynamic epistemic logic[END_REF], we also plan to study several dynamic extensions of our logic in order to capture a large variety of cognitive dynamics in a multi-agent setting. The latter includes belief change, desire change and choice change. We believe choice change is particularly interesting given the dependence of an agent's choices on her beliefs and desires, as illustrated in Section 3.3. Specifically, since an agent's choices depend on her plausibility and desirability orderings over possible worlds, if these orderings change, then the agent's choices may also change. In other words, choice change can be seen as derivative of belief change and desire change. Another research direction we plan to follow in the future is to connect the notion of choice formalized in Section 3.3 with a notion of action in the sense of STIT logic, the logic of "seeing to it that" by [START_REF] Belnap | Facing the future: agents and choices in our indeterminist world[END_REF]. The interesting aspect of STIT is that agents' choices are explicit in its semantics and agents' actions are conceived as results of their choices.

A.2 Proof of Lemma 3

Proof. Let us first prove that (

i) if x ∈ Σ and ϕ ∈ Σ then [π](x → ϕ) ∈ Σ. Suppose x, ϕ ∈ Σ. Thus, x ∧ ϕ ∈ Σ since Σ is a MCT. Moreover, (x ∧ ϕ) → [π](x → ϕ) ∈ Σ, because of Axiom Mostx. Hence, [π](x → ϕ) ∈ Σ.
Now let us prove by absurdum that (ii) if x ∈ Σ, Σ and ΣR c π Σ then Σ = Σ . Suppose x ∈ Σ, Σ , ΣR c π Σ and Σ = Σ . The latter implies that there exists ϕ such that ϕ ∈ Σ and ϕ ∈ Σ . By item (i) above, it follows that [π](x → ϕ) ∈ Σ. Since ΣR c π Σ , the latter implies that x → ϕ ∈ Σ . Since x ∈ Σ , it follows that ϕ ∈ Σ which leads to a contradiction.

A.3 Proof of Lemma 4

Proof. Suppose w is a MCT and π ϕ ∈ w. It follows that [π]w = {ψ : [π]ψ ∈ w} is a consistent theory. Indeed, it is easy to check that [π]w contains all theorems of DLCA, is closed under modus ponens and rule Cov. Let us prove that it is consistent by reductio ad absurdum. Suppose

A.4 Proof of Lemma 6

Proof. The fact that M c satisfies Constraints C3 and C4 * follows from Lemma 2 and Lemma 3. To prove that ≡i is an equivalence relation that c i,D and c i,D are preorders and that M c satisfies Constraints C1 and C2 is just a routine exercise. Indeed, Axioms T≡ i , 4≡ i , 5≡ i , T i,τ , 4 i,τ Int i,τ ,≡ i and Conn i,τ ,≡ i are canonical for these semantic conditions.

To conclude, we need to prove that the following six conditions hold, for i ∈ Agt and τ ∈ {P, D}: We only prove the second and fourth conditions which are the most difficult ones to prove. Let us start with the proof of the second condition. The right-to-left direction is standard. We only prove the left-to-right direction. Suppose (w, v) ∈ R c π;π . Let [π]w = {ψ : [π]ψ ∈ w}. Moreover, let π v = { π ψ : ψ ∈ v}. Finally, let π ψ1, π ψ2, . . . be an enumeration of the elements of π v. We define Σ 1 = [π]w + π ψ1 and, for all k > 1, Σ k = Σ k-1 + π ψ k . By Lemma 10 and the fact that [π]w is a theory, it can be shown that every Σ k is a theory. Moreover, by induction on k, it can be shown that every Σ k is consistent. Since Σ k-1 ⊆ Σ k for all k > 1, it follows that Σ = k>1 Σ k-1 is a consistent theory. By Lemma 1 and the definition of Σ, there exists u ∈ W c such that Σ ⊆ u, (w, u) ∈ R c π and (u, v) ∈ R c π . Let us now prove the fourth condition. Suppose (w, v) ∈ R c π∩π . By Definition 15 and Proposition 11, it follows that, for all ϕ, if ϕ ∈ v then π ∩ π ϕ ∈ w. The latter implies that for all ϕ, if ϕ ∈ v then π ∩π (ϕ∨⊥) ∈ w since π ∩π ϕ → π ∩π (ϕ∨⊥). By Axiom Kπ, it follows that, for all ϕ, if ϕ ∈ v then π ϕ ∨ π ⊥ ∈ w. Thus, for all ϕ, if ϕ ∈ v then π ϕ ∈ w, since ( π ϕ ∨ π ⊥) → π ϕ. In a similar way, we can prove that, for all ϕ, if ϕ ∈ v then π ϕ ∈ w. By Definition 15 and Proposition 11, it follows that (w, v) ∈ R c π and (w, v) ∈ R c π . Now suppose (w, v) ∈ R c π and (w, v) ∈ R c π . Thus, by Definition 15 and Proposition 11, (i) for all ϕ, if ϕ ∈ v then π ϕ ∈ w and π ϕ ∈ w. By Proposition 11 and Lemma 2, we have that (ii) there exists x ∈ Num such that, for all ϕ, ϕ ∈ v iff x ∧ ϕ ∈ v. Item (i) and item (ii) together imply that (iii) there exists x ∈ Num such that, for all ϕ, if ϕ ∈ v then π (x ∧ ϕ) ∈ w and π (x ∧ ϕ) ∈ w. We are going to prove the following theorem:

(w, v) ∈ R c ∼ i,τ iff (w, v) ∈ R c ≡ i and (w, v) ∈ R c i,τ (w, v) ∈ R c π;π iff ∃u ∈ W c : (w, u) ∈ R c π and (u, v) ∈ R c π (w, v) ∈ R c π∪π iff (w, v) ∈ R c π or (w, v) ∈ R c π (w, v) ∈ R c π∩π iff (w, v) ∈ R c π and (w, v) ∈ R c π (w, v) ∈ R c -π iff (v, w) ∈ R c
( π (x ∧ ϕ) ∧ π (x ∧ ϕ)) → π ∩ π (x ∧ ϕ)
By Axiom Kπ, π (x∧ϕ)∧ π (x∧ϕ) implies π x∧ π x. By Axiom Add2∩, the latter implies π ∩π x. Moreover, by Axiom Int i,τ ,≡ i and Axiom Mostx, π (x∧ϕ) implies [≡ ∅ ](x → ϕ). By Axiom Int i,τ ,≡ i , the latter implies [π ∩ π ](x → ϕ). By Axiom Kπ, [π ∩ π ](x → ϕ) and π ∩π x together imply π ∩π (x∧ϕ). Thus, π (x∧ϕ)∧ π (x∧ϕ) implies π ∩π (x∧ϕ).

From previous item (iii) and the previous theorem it follows that there exists x ∈ Num such that, for all ϕ, if ϕ ∈ v then π ∩ π (x ∧ ϕ). The latter implies that, for all ϕ, if ϕ ∈ v then π ∩ π ϕ. The latter implies that (w, v) ∈ R c π∩π .

  ⊥ ∈ [π]w. Thus, [π]⊥ ∈ w. Hence, [π]¬ϕ ∈ w. Since π ϕ ∈ w, ⊥ ∈ w. The latter contradicts the fact that w is a MCT. Let us distinguish two cases. Case 1: ϕ ∈ [π]w. Thus, ¬ϕ ∈ [π]w since w is consistent. Thus, by Lemma 1, there exists MCT v such that [π]w ⊆ v, ϕ ∈ v and ¬ϕ ∈ v. By definition of R c π , wR c π v. Case 2: ϕ ∈ [π]w. By Lemma 10, [π]w + ϕ is a theory since [π]w is a theory. [π]w + ϕ is consistent. Suppose it is not. Thus, ϕ → ⊥ ∈ [π]w and, consequently, ¬ϕ ∈ [π]w. Hence, [π]¬ϕ ∈ w. It follows that ⊥ ∈ w, since π ϕ ∈ w. But this contradicts the fact that w is a MCT. Thus, [π]w + ϕ is a consistent theory. Moreover, ϕ ∈ [π]w + ϕ, ¬ϕ ∈ [π]w + ϕ and [π]w ⊆ [π]w + ϕ. By Lemma 1, there exists MCT v such that [π]w ⊆ v, ϕ ∈ v and ¬ϕ ∈ v. By definition of R c π , wR c π v.

  π wR c ϕ? v iff w = v and M c , w |= ϕ

This means that there could be a world v such that w ≡i v and there is a i,P -infinite ascending chain from v.

This means that there could be a world v such that w ≡i v and there is a i,D -infinite descending chain from v.

[START_REF] Baltag | Talking your way into agreement: Belief merge by persuasive communication[END_REF] According to deontic logicians, there are at least two candidate readings of the statement "ϕ is permitted": (i) every instance of ϕ is OK according to the normative regulation, and (ii) at least one instance of ϕ (but possibly not all) is OK according to the normative regulation. The former is the so-called open reading of permission.

Acknowledgments

This work was supported by the ANR project CoPains. I would like to thank Philippe Balbiani for his useful comments on its content.

In this section, we provide a sound and complete axiomatization for the logic DLCA. The first step consists in precisely defining this logic. Definition 12. We define DLCA to be the extension of classical propositional logic given by the following axioms and rules with τ ∈ {P, D}:

For every ϕ ∈ L DLCA , we write ϕ to denote the fact that ϕ is a theorem of DLCA, i.e., there exists an at most countably infinite sequence ψ 0 , ψ 1 , . . . such that ψ 0 = ϕ and for all k ≥ 0, ψ k is an instance of some axiom or ψ k can be obtained from some later members of the sequence by an application of some inference rule.

The rest of this section is devoted to prove that the logic DLCA is sound and complete for the class of multi-agent cognitive models.

Soundness, namely checking that the axioms are valid and the the rules of inferences preserve validity, is a routine exercise. Notice that the admissibility of the rule of inference Cov is guaranteed by the fact that the set of nominals Nom is infinite.

As for completeness, the proof is organized in several steps. We use techniques from dynamic logic and modal logic with names [START_REF] Passy | An essay in combinatorial dynamic logic[END_REF][START_REF] Gargov | Modal logic with names[END_REF].

In the rest of this section, we denote sets of formulas from L DLCA by Σ, Σ , . . .. Let ϕ ∈ L DLCA and Σ ⊆ L DLCA , we define:

Let us start by defining the concepts of theory and maximal consistent theory. Definition 13. A set of formulas Σ is said to be a theory if it contains all theorems of DLCA and is closed under modus ponens and rule Cov. It is said to be a consistent theory if it is a theory and ⊥ ∈ Σ. It is said to be a maximal consistent theory (MCT) if it is a consistent theory and, for each consistent theory Σ , we have that if Σ ⊆ Σ then Σ = Σ .

We have the following property for theories.

Proposition 10. Let Σ be a theory and let ϕ ∈ L DLCA . Then, Σ + ϕ is a theory. Moreover, if Σ is consistent then either Σ + ϕ is consistent or Σ + ¬ϕ is consistent.

The following proposition highlights some standard properties of MCTs.

Proposition 11. Let Σ be a MCT. Then, for all ϕ, ψ ∈ L DLCA :

The following variant of the Lindenbaum's lemma is proved in the same way as [START_REF] Passy | An essay in combinatorial dynamic logic[END_REF]Lemma 4.15]. Lemma 1. Let Σ be a consistent theory and let ϕ ∈ Σ. Then, there exists a MCT Σ + such that Σ ⊆ Σ + and ϕ ∈ Σ + .

The following lemma highlights a fundamental properties of MCTs.

Lemma 2. Let Σ be a MCT. Then, there exists x ∈ Num such x ∈ Σ.

Let us now define the canonical model for our logic.

Definition 14. The canonical model is the tuple M

-W c is the set of all MCTs, for all i ∈ Agt, for all τ ∈ {P, D}, for all w, v ∈ W c ,

Let us now define the canonical relations for the complex programs π.

) be the canonical model. Then, for all π ∈ P and for all w, v ∈ W c :

The following Lemma 3 highlights one fundamental property of the canonical model.

) be the canonical model. Then, for all Σ, Σ ∈ W c , for all π ∈ P and for all x ∈ Num, if x ∈ Σ, x ∈ Σ and ΣR c π Σ then Σ = Σ .

The next step consists in proving the following existence lemma.

The following truth lemma is proved in the usual way by induction on the structure of ϕ thanks to Lemma 4.

The pre-final stage of the proof consists in introducing an alternative semantics for the language L DLCA which turns out to be equivalent to the original semantics based on MCMs.

Definition 16 (Quasi multi-agent cognitive model). A quasi multi-agent cognitive model (quasi-MCM) is a tuple M = (W, ( i,P ) i∈Agt , ( i,D ) i∈Agt , (≡ i ) i∈Agt , V ) where W , i,P , i,D , ≡ i and V are as in Definition 1 except that Constraint C4 is replaced by the following weaker constraint. For all w, v ∈ W :

and wR π v for some π ∈ P then w = v.

By the generated submodel property, it is easy to show that the semantics in terms of MCMs and the semantics in terms of quasi-MCMs are equivalent with respect to the language L DLCA .

Proposition 12. Let ϕ ∈ L DLCA . Then, ϕ is valid relative to the class of MCMs if and only if ϕ is valid relative to the class of quasi-MCMs.

The following theorem highlights that the canonical model is indeed a structure of the right type. Lemma 6. The canonical model M c is a quasi-MCM.

Let us conclude the proof by supposing ¬ϕ. Therefore, by Lemma 1 and the fact that the set of DLCA-theorems is a consistent theory, there exists a MCT w such that ¬ϕ ∈ w. Thus, by Proposition 11, we can find a MCT w such that ϕ ∈ w. By Lemma 5, the latter implies M c , w |= ϕ for some w ∈ W c . Since, by Lemma 6, M c is a quasi-MCM, it follows that ϕ is satisfiable relative to the class of quasi-MCMs. Therefore, by Proposition 12, ϕ is satisfiable relative to the class of MCMs.

We can finally state the main result of this section.

Theorem 1. The logic DLCA is sound and complete for the class of multi-agent cognitive models.