Cognitive Aspects in Epistemic Logic L-DINF⋆ Stefania Costantini1,3 , Andrea Formisano2,3,* and Valentina Pitoni1 1 Università di L’Aquila (DISIM), Via Vetoio, 1, L’Aquila, 67100, Italy 2 Università di Udine (DMIF), Via delle Scienze, 206, Udine, 33100, Italy 3 INdAM — GNCS, Piazzale Aldo Moro, 5, Roma, 00185, Italy Abstract In this paper, we report about a line of work aimed to formally model via a logical framework —the Logic of “Inferable” L-DINF— (aspects of) the group dynamics of cooperative agents. We outline, in particular, the cognitive aspects built within our logic, that consist in features allowing a designer to model real-world situations encompassing joint intentions and plans with roles, preferences and costs concerning action execution, and involving aspects of a Theory of Mind, i.e., the ability to reason about beliefs of others. Keywords Epistemic Logic, Cognitive Aspect, Multi-Agent Systems, Cooperation and Roles assignment 1. Introduction Agents and Multi-Agent Systems (MAS) have been widely adopted in Artificial Intelligence (AI) to model societies whose members are to some extent cooperative towards each other. Agents belonging to a MAS can be able to achieve better results via cooperation, because it is often the case that a group can fulfil objectives that are out of reach for a single agent. To this aim, it is useful for agents to be able to reason about what their group of agents can do, and what they can do within a group (including leaving/joining groups). In this paper, we present a logical framework (the Logic of “Inferable” L-DINF [1]) that we have proposed and extended over the years, defined originally as an extension of a pre-existing epistemic logic by Lorini & Balbiani. In L-DINF, groups of cooperative agents can jointly perform actions and reach goals. We outline, in particular, the cognitive aspects built within such a logic. In L-DINF, our overall objective has been to devise an agent-oriented logical framework that allows a designer to formalize and formally verify MAS, modelling the capability to construct and execute joint plans within a group of agents. We have devoted all along a special attention to explainability, in the perspective of Trustworty AI and to cognitive aspect. In the logic, we have considered actions’ cost, and agents’ budget, where an agent able to perform an action but not owning the needed budget can be supported by its group to cover the cost. The group takes into consideration the preferences that each agent can have for what concerns performing each action. We have also introduced agents’ roles within a group, in terms IJCAI 22 Workshop: Cognitive Aspects of Knowledge Representation, July 23-29, 2022, Messe Wien, Vienna, Austria * Corresponding author. stefania.costantini@univaq.it (S. Costantini); andrea.formisano@uniud.it (A. Formisano); valentina.pitoni@univaq.it (V. Pitoni)  0000-0002-5686-6124 (S. Costantini); 0000-0002-6755-9314 (A. Formisano); 0000-0002-4245-4073 (V. Pitoni) © 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) of the actions that each agent is allowed to perform in the context of the group. All these features are defined in a modular way, so as to be composed to model different group behaviours. For instance, normally an action can be performed only by an agent which is able and allowed to perform it; but, in exceptional circumstances, for lack of alternatives, also by an agent that is able, although not allowed, to perform it. Naturally, we devised a full syntax and semantics and the proof of strong completeness of our logic w.r.t. its canonical model. Many kinds of logical frameworks can be found in the literature which try to emulate cognitive aspects of human beings, also from the cooperative point of view. However, what distinguishes our approach from related ones is that many key aspects are not specified in the logical theory defining an agent: rather, we introduce special functions in the definitions of model and of canonical model. For the practical realization of such functions, we envisage separate modules from which agent’s logical theory “inputs” the results. Such modules might be specified even in some other logic or also, pragmatically, via pieces of code. Other conditions such as, e.g., feasibility of actions, are also defined modularly, as they concern aspects that should be verified contextually, according to agents’ environmental conditions. In recent work [2], we considered that there are classes of applications where agents can profit from the ability to represent group dynamics, and to understand the behaviour of others; i.e., agents should be able to assess or hypothesize what other agents (including human users) believe and intend to do. This accounts to be able to represent aspects of “Theory of Mind”, which is the set of social-cognitive skills involving: the ability to attribute mental states, including desires, beliefs, and knowledge, to oneself and to other agents; and, importantly, the ability to reason about the practical consequences of such mental states. Such ability is crucial for prediction and interpretation of other agents’ behavioural responses (cf. Oxford Handbook of Philosophy and Cognitive Science [3], Chapter by Alvin I. Goldman). Thus, we have devised an extension of L-DINF able to represent aspects of Theory of Mind. Our motivation lies in our related research work in agent-oriented programming languages. In particular, our research group has defined the language DALI [4, 5, 6], which has been fully implemented [7] and is endowed with a fully logical semantics [8]. DALI has been applied in many applications, among which cognitive robotics [9] and eHealth [10, 11]: in such application fields, a socially and psychologically acceptable interaction with the user is required, whence our aim to develop a suitable logical formalization of (at least a basic version of) ToM to be in perspective incorporated into DALI semantics and implementation. In [12] we have thoroughly discussed the relationship of logic L-DINF with related work, so we refer the reader to that paper for this point. The paper is organized as follows. In Section 2 we introduce syntax and semantics of L-DINF. Sections 3 and 4 discuss significant examples of application of the new logic, concerning cognitive aspects. The first considers how to tune group’s behaviour according to circumstances; the second concerns how to represent aspects of the Theory of Mind Finally, in Section 5 we conclude. 2. Logical Framework L-DINF is a logic which consists of a static component and a dynamic one. The static component, called L-INF, is a logic of explicit beliefs and background knowledge. The dynamic component, called L-DINF, extends the static one with dynamic operators capturing the consequences of the agents’ inferential actions on their explicit beliefs as well as a dynamic operator capturing what an agent can conclude by performing some inferential action in its repertoire. 2.1. Syntax In this section we provide and illustrate the syntax of the proposed logic. Let Atm = {𝑝, 𝑞, . . .} be a countable set of atomic propositions. By 𝑃 𝑟𝑜𝑝 we denote the set of all propositional formulas, i.e. the set of all Boolean formulas built out of the set of atomic propositions Atm. The set 𝐴𝑡𝑚𝐴 represents the set of physical actions that agents can perform, including “active sensing” actions (e.g., “let’s check whether it rains”, “let’s measure the temperature”). Let Agt be a set of 𝑛 agents identified, for simplicity, by integer numbers: Agt = {1, 2, . . . , 𝑛}. The language of L-DINF, denoted by ℒL-DINF , is defined by the following grammar: 𝜙, 𝜓 ::= 𝑝 | ¬𝜙 | 𝜙 ∧ 𝜓 | B𝑖 𝜙 | K𝑖 𝜙 | 𝑑𝑜𝑖 (𝜑𝐴 ) | 𝑑𝑜𝑃𝑖 (𝜑𝐴 ) | 𝑐𝑎𝑛_𝑑𝑜𝑖 (𝜑𝐴 ) | 𝑑𝑜𝐺 (𝜑𝐴 ) | 𝑑𝑜𝑃𝐺 (𝜑𝐴 ) | 𝑐𝑎𝑛_𝑑𝑜𝐺 (𝜑𝐴 ) | intend 𝑖 (𝜑𝐴 ) | intend 𝐺 (𝜑𝐴 ) | exec 𝑖 (𝛼) | exec 𝐺 (𝛼) | [𝐺:𝛼] 𝜙 | pref _do 𝑖 (𝜑𝐴 , 𝑑) | pref _do 𝐺 (𝑖, 𝜑𝐴 ) | 𝛼 ::= ⊢(𝜙,𝜓) | ∩(𝜙,𝜓) | ↓(𝜙, 𝜓) | ⊣(𝜙, 𝜓) where 𝑝 ranges over Atm, 𝑖 ∈ Agt, 𝐺 ⊆ Agt, 𝜑𝐴 ∈ 𝐴𝑡𝑚𝐴 , and 𝑑 ∈ N. Other Boolean operators are defined from ¬ and ∧ in the standard manner. Moreover, for simplicity, whenever 𝐺 = {𝑖} we will write 𝑖 as subscript in place of {𝑖}. So, for instance, we often write pref _do 𝑖 (𝑖, 𝜑𝐴 ) instead of pref _do {𝑖} (𝑖, 𝜑𝐴 ) and similarly for other constructs. The language of inferential actions of type 𝛼 is denoted by ℒACT . The static part L-INF of L-DINF, includes only those formulas not having sub-formulas of type 𝛼, namely, no inferential operation is admitted. Notice that, the framework we are introducing is propositional, but, to simplify the description, we will often write elements of Atm and of Atm 𝐴 as structured expressions, such as 𝑖𝑛(𝑑𝑜𝑙𝑙, 𝑏𝑜𝑥), 𝑖𝑛(𝑑𝑜𝑙𝑙, 𝑏𝑎𝑠𝑘𝑒𝑡), or 𝑝𝑢𝑡𝐴 (𝑑𝑜𝑙𝑙, 𝑏𝑜𝑥). Notice, moreover, that we do not consider in this paper the possibility that an agent has belief or knowledge involving nesting of modalities. Hence, in formulas of the forms B𝑖 𝜙 and K𝑖 𝜙, the subformula 𝜙 does not involve any modal operator B𝑗 and K𝑗 (for any 𝑖, 𝑗). We consider the set of agents as partitioned in groups: each agent 𝑖 always belongs to a single group 𝐺 ⊆ Agt. Any agent 𝑖, at any time, can perform a (physical) action joinA (𝑖, 𝑗), for 𝑗 ∈ Agt, in order to change its group and join 𝑗’s group. Before introducing the formal semantics let us briefly describe the intended informal meaning of basic formulas of L-INF. Expressions of the form intend 𝑖 (𝜑𝐴 ), where 𝜑𝐴 ∈ 𝐴𝑡𝑚𝐴 , indicate the intention of agent 𝑖 to perform the action 𝜑𝐴 in the sense of the BDI agent model [13]. This intention can be part of an agent’s knowledge base from the beginning, or it can be derived later. In this paper we do not cope with the formalization of BDI, for which the reader may refer, e.g., to [14]. So, we will treat intentions rather informally, assuming also that intend 𝐺 (𝜑𝐴 ) holds whenever all agents in group 𝐺 intend to perform action 𝜑𝐴 . The formula doi (𝜑𝐴 ), where again we require that 𝜑𝐴 ∈ 𝐴𝑡𝑚𝐴 , indicates actual execution of action 𝜑𝐴 by agent 𝑖, automatically recorded by the new belief 𝑑𝑜𝑃𝑖 (𝜑𝐴 ) (postfix “𝑃 ” standing for “past” action). By precise choice, do and do P (and similarly doG and doG P ) are not axiomatized. In fact, they are realized by what has been called in [15] a semantic attachment, i.e., a procedure which connects an agent with its external environment in a way that is unknown at the logical level. The axiomatization concerns only the relationship between doing and being enabled to do. The expressions can_doi (𝜑𝐴 ) and pref _do 𝑖 (𝜑𝐴 , 𝑑) (where it is required that 𝜑𝐴 ∈ 𝐴𝑡𝑚𝐴 ) are closely related to doi (𝜑𝐴 ). In fact, can_doi (𝜑𝐴 ) is to be seen as an enabling condition, indicating that agent 𝑖 is enabled to execute action 𝜑𝐴 , while instead pref _doi (𝜑𝐴 , 𝑑) indicates the level 𝑑 of preference/willingness of agent 𝑖 to perform that action. The expression pref _doG (𝑖, 𝜑𝐴 ) indicates that agent 𝑖 exhibits the maximum level of preference on performing action 𝜑𝐴 among all members of its group 𝐺. Notice that, if a group of agents intends to perform an action 𝜑𝐴 , this will entail that the entire group intends to do 𝜑𝐴 , that will be enabled to be actually executed only if at least one agent 𝑖 ∈ 𝐺 can do it, i.e., it can derive can_doi (𝜑𝐴 ). Unlike explicit beliefs, i.e., facts and rules acquired via perceptions during an agent’s operation and kept in the working memory, an agent’s background knowledge is assumed to satisfy omni- science principles, such as closure under conjunction and known implication, and closure under logical consequence, and introspection. In fact, K𝑖 is actually the well-known S5 modal operator often used to model/represent knowledge. The fact that background knowledge is closed under logical consequence is justified because we conceive it as a kind of stable reliable knowledge base, or long-term memory. We assume the background knowledge to include: facts (formulas) known by the agent from the beginning, and facts the agent has later decided to store in its long-term memory (by means of some decision mechanism not treated here) after having processed them in its working memory. We therefore assume background knowledge to be irrevocable, in the sense of being stable over time. A formula of the form [𝐺 : 𝛼] 𝜙, with 𝐺 ⊆ Agt, and where 𝛼 must be an inferential action, states that “𝜙 holds after action 𝛼 has been performed by at least one of the agents in 𝐺, and all agents in 𝐺 have common knowledge about this fact”. We distinguish four types of inferential actions 𝛼 which allow us to capture some of the dynamic properties of explicit beliefs and background knowledge: ↓(𝜙, 𝜓), ∩(𝜙,𝜓), ⊣(𝜙, 𝜓), and ⊢(𝜙,𝜓). These actions characterize the basic operations of forming explicit beliefs via inference: • ↓(𝜙, 𝜓): this inferential action infers 𝜓 from 𝜙, in case 𝜙 is believed and, according to agent’s background knowledge, 𝜓 is a logical consequence of 𝜙. I.e., by performing this inferential action, an agent tries to retrieve from its background knowledge in long-term memory the information that 𝜙 implies 𝜓 and, if it succeeds, it starts believing 𝜓. • ∩(𝜙,𝜓): closes the explicit belief 𝜙 and the explicit belief 𝜓 under conjunction. I.e., 𝜙 ∧ 𝜓 is deduced from the explicit beliefs 𝜙 and 𝜓. • ⊣(𝜙, 𝜓): this inferential action performs a simple form of “belief revision”. It removes 𝜓 from the working memory in case 𝜙 is believed and, according to agent’s background knowledge, ¬𝜓 is logical consequence of 𝜙. Both 𝜓 and 𝜙 are required to be ground atoms. • ⊢(𝜙,𝜓): adds 𝜓 to the working memory in case 𝜙 is believed and, according to agent’s working memory, 𝜓 is logical consequence of 𝜙. Differently from ↓(𝜙, 𝜓), this action oper- ates on the working memory without retrieving anything from the background knowledge. Formulas of the forms execi (𝛼) and exec 𝐺 (𝛼) express executability of inferential actions either by agent 𝑖, or by a group 𝐺 of agents (which is a consequence of any of the group members being able to execute the action). It has to be read as: “𝛼 is an inferential action that agent 𝑖 (resp. an agent in 𝐺) can perform”. Remark 1. In the mental actions ⊢ (𝜙,𝜓) and ↓(𝜙, 𝜓), the formula 𝜓 which is inferred and asserted as a new belief can be 𝑐𝑎𝑛_𝑑𝑜𝑖 (𝜑𝐴 ) or 𝑑𝑜𝑖 (𝜑𝐴 ), which denote the possibility of ex- ecution or actual execution of physical action 𝜑𝐴 . We assume that when inferring 𝑑𝑜𝑖 (𝜑𝐴 ) (from 𝑐𝑎𝑛_𝑑𝑜𝑖 (𝜑𝐴 ) and possibly other conditions) then the action is actually executed, and the corresponding belief 𝑑𝑜𝑃𝑖 (𝜑𝐴 ) is asserted, possibly augmented with a time-stamp. Actions are supposed to succeed by default; in case of failure, a corresponding failure event will be perceived by the agent. The 𝑑𝑜𝑃𝑖 beliefs constitute a history of the agent’s operation, so they might be useful for the agent to reason about its own past behaviour, and/or, importantly, they may be useful to provide explanations to human users. Remark 2. Explainability in our approach can be directly obtained from proofs. Let us assume for simplicity that inferential actions can be represented in infix form as 𝜙𝑗 𝑂𝑃 𝜙𝑗+1 for some 𝑗. Also, for agent 𝑖, execi (𝛼) means that the mental action 𝛼 is executable by the agent and it is indeed executed. If, for instance, the user wants an explanation of why the action 𝜑𝐴 has been performed, (︀ the system can exhibit the proof that has lead to 𝜑𝐴 , put in the explicit form: execi (𝜙1 𝑂𝑃)︀1 𝜙2 ) ∧ . . . ∧ execi (𝜙𝑛−1 𝑂𝑃𝑛 𝜙𝑛 ) ∧ execi (𝜙𝑛 𝑂𝑃𝑛 𝑐𝑎𝑛_𝑑𝑜𝑖 (𝜑𝐴 ))∧ 𝑖𝑛𝑡𝑒𝑛𝑑𝑖 (𝜑𝐴 ) ⊢ 𝑑𝑜𝑖 (𝜑𝐴 ) where each 𝑂𝑃𝑘 is one of the (mental) actions discussed above. The proof can possibly be translated into natural language, and declined either top-down or bottom-up. As said in the Introduction, we model agents which, to execute an action, may have to pay a cost, so they must have a consistent budget available. Moreover, agents are entitled to perform only those physical actions that they conclude they can do. Agents belonging to a group are assumed to be cooperative. An action can be executed by a group if at least one agent in the group is able to execute it, and the group has the necessary budget available, sharing the cost according to some policy. The cooperative nature of our agents manifests itself also in selecting, among the agents that are able to do some physical action, the one(s) which best prefer to perform that action. We do not have introduced costs and budget, feasibility of actions and willingness to perform them, in the language for two reasons: to keep the complexity of the logic reasonable, and to make such features customizable in a modular way. For instance, cost-sharing policies different from the one that we will show below might easily be introduced, even different ones for different resources. 2.2. Semantics Definition 2.1 introduces the notion of L-INF model, which is then used to introduce semantics of the static fragment of the logic. Notice that many relevant aspects of an agent’s behaviour are specified in the definition of L-INF model, including which mental and physical actions an agent can perform, which is the cost of an action and which is the budget that the agent has available, which is the preference degree of the agent to perform each action. This choice has the advantage of keeping the complexity of the logic under control, and of making these aspects modularly modifiable. In this paper, we introduce new function 𝐻 that, for each agent 𝑖 belonging to a group, enables the agent to perform a certain set of actions, so, in this way, it specifies the role of 𝑖 within the group. As before let Agt be the set of agents. Definition 2.1. A model is a tuple 𝑀 = (𝑊, 𝑁, ℛ, 𝐸, 𝐵, 𝐶, 𝐴, 𝐻, 𝑃, 𝑉 ) where: • 𝑊 is a set of worlds (or situations); • ℛ = {𝑅𝑖 }𝑖∈Agt is a collection of equivalence relations on 𝑊 : 𝑅𝑖 ⊆ 𝑊 × 𝑊 for each 𝑖 ∈ Agt; 𝑊 • 𝑁 : Agt × 𝑊 −→ 22 is a neighborhood function such that, for each 𝑖 ∈ Agt, each 𝑤, 𝑣 ∈ 𝑊 , and each 𝑋 ⊆ 𝑊 these conditions hold: (C1) if 𝑋 ∈ 𝑁 (𝑖, 𝑤) then 𝑋 ⊆ {𝑣 ∈ 𝑊 | 𝑤𝑅𝑖 𝑣}, (C2) if 𝑤𝑅𝑖 𝑣 then 𝑁 (𝑖, 𝑤) = 𝑁 (𝑖, 𝑣); • 𝐸 : Agt × 𝑊 −→ 2ℒACT is an executability function of mental actions such that, for each 𝑖 ∈ Agt and 𝑤, 𝑣 ∈ 𝑊 , it holds that: (D1) if 𝑤𝑅𝑖 𝑣 then 𝐸(𝑖, 𝑤) = 𝐸(𝑖, 𝑣); • 𝐵 : Agt × 𝑊 −→ N is a budget function such that, for each 𝑖 ∈ Agt and 𝑤, 𝑣 ∈ 𝑊 , the following holds (E1) if 𝑤𝑅𝑖 𝑣 then 𝐵(𝑖, 𝑤) = 𝐵(𝑖, 𝑣); • 𝐶 : Agt × ℒACT × 𝑊 −→ N is a cost function such that, for each 𝑖 ∈ Agt, 𝛼 ∈ ℒACT , and 𝑤, 𝑣 ∈ 𝑊 , it holds that: (F1) if 𝑤𝑅𝑖 𝑣 then 𝐶(𝑖, 𝛼, 𝑤) = 𝐶(𝑖, 𝛼, 𝑣); • 𝐴 : Agt × 𝑊 −→ 2𝐴𝑡𝑚𝐴 is an executability function for physical actions such that, for each 𝑖 ∈ Agt and 𝑤, 𝑣 ∈ 𝑊 , it holds that: (G1) if 𝑤𝑅𝑖 𝑣 then 𝐴(𝑖, 𝑤) = 𝐴(𝑖, 𝑣); • 𝐻 : Agt × 𝑊 −→ 2𝐴𝑡𝑚𝐴 is an enabling function for physical actions such that, for each 𝑖 ∈ Agt and 𝑤, 𝑣 ∈ 𝑊 , it holds that: (G2) if 𝑤𝑅𝑖 𝑣 then 𝐻(𝑖, 𝑤) = 𝐻(𝑖, 𝑣); • 𝑃 : Agt × 𝑊 × 𝐴𝑡𝑚𝐴 −→ N is a preference function for physical actions 𝜑𝐴 such that, for each 𝑖 ∈ Agt and 𝑤, 𝑣 ∈ 𝑊 , it holds that: (H1) if 𝑤𝑅𝑖 𝑣 then 𝑃 (𝑖, 𝑤, 𝜑𝐴 ) = 𝑃 (𝑖, 𝑣, 𝜑𝐴 ); • 𝑉 : 𝑊 −→ 2Atm is a valuation function. To simplify the notation, let 𝑅𝑖 (𝑤) denote the set {𝑣 ∈ 𝑊 | 𝑤𝑅𝑖 𝑣}, for 𝑤 ∈ 𝑊 . The set 𝑅𝑖 (𝑤) identifies the situations that agent 𝑖 considers possible at world 𝑤. It is the epistemic state of agent 𝑖 at 𝑤. In cognitive terms, 𝑅𝑖 (𝑤) can be conceived as the set of all situations that agent 𝑖 can retrieve from its long-term memory and reason about. While 𝑅𝑖 (𝑤) concerns background knowledge, 𝑁 (𝑖, 𝑤) is the set of all facts that agent 𝑖 explicitly believes at world 𝑤, a fact being identified with a set of worlds. Hence, if 𝑋 ∈ 𝑁 (𝑖, 𝑤) then, the agent 𝑖 has the fact 𝑋 under the focus of its attention and believes it. We say that 𝑁 (𝑖, 𝑤) is the explicit belief set of agent 𝑖 at world 𝑤. The executability of inferential actions is determined by the function 𝐸. For an agent 𝑖, 𝐸(𝑖, 𝑤) is the set of inferential actions that agent 𝑖 can execute at world 𝑤. The value 𝐵(𝑖, 𝑤) is the budget the agent has available to perform inferential actions. The value 𝐶(𝑖, 𝛼, 𝑤) is the cost to be paid by agent 𝑖 to execute the inferential action 𝛼 in the world 𝑤. 𝑁 (𝑖, 𝑤) and 𝐵(𝑖, 𝑤) are updated whenever a mental action is performed, and this changes are described in [16]. The executability of physical actions is determined by the function 𝐴. For an agent 𝑖, 𝐴(𝑖, 𝑤) is the set of physical actions that agent 𝑖 can execute at world 𝑤. 𝐻(𝑖, 𝑤) instead is the set of physical actions that agent 𝑖 is enabled by its group to perform. Which means, 𝐻 defines the role of an agent in its group, via the actions that it is allowed to execute. Agent’s preference on executability of physical actions is determined by the function 𝑃 . For an agent 𝑖, and a physical action 𝜑𝐴 , 𝑃 (𝑖, 𝑤, 𝜑𝐴 ) is an integer value 𝑑 indicating the degree of willingness of agent 𝑖 to execute 𝜑𝐴 at world 𝑤. Constraint (C1) imposes that agent 𝑖 can have explicit in its mind only facts which are compatible with its current epistemic state. Moreover, according to constraint (C2), if a world 𝑣 is compatible with the epistemic state of agent 𝑖 at world 𝑤, then agent 𝑖 should have the same explicit beliefs at 𝑤 and 𝑣. In other words, if two situations are equivalent as concerns background knowledge, then they cannot be distinguished through the explicit belief set. This aspect of the semantics can be extended in future work to allow agents make plausible assumptions. Analogous properties are imposed by constraints (D1), (E1), and (F1). Namely, (D1) imposes that agent 𝑖 always knows which inferential actions it can perform and those it cannot. (E1) states that agent 𝑖 always knows the available budget in a world (potentially needed to perform actions). (F1) determines that agent 𝑖 always knows how much it costs to perform an inferential action. (G1) and (H1) determine that an agent 𝑖 always knows which physical actions it can perform and those it cannot, and with which degree of willingness, where (G2) specifies that an agent also knows whether its group gives it the permission to execute a certain action or not, i.e., if that action pertains to its role in the group. Truth values of L-DINF formulas are inductively defined as follows. Given a model 𝑀 = (𝑊, 𝑁, ℛ, 𝐸, 𝐵, 𝐶, 𝐴, 𝐻, 𝑃, 𝑉 ), 𝑖 ∈ Agt, 𝐺 ⊆ Agt, 𝑤 ∈ 𝑊 , and a formula 𝜙 ∈ ℒL-INF , we introduce the following shorthand notation: ‖𝜙‖𝑀 𝑖,𝑤 = {𝑣 ∈ 𝑊 : 𝑤𝑅𝑖 𝑣 and 𝑀, 𝑣 |= 𝜙} whenever 𝑀, 𝑣 |= 𝜙 is well-defined (see below). Then, we set: (t1) 𝑀, 𝑤 |= 𝑝 iff 𝑝 ∈ 𝑉 (𝑤) (t2) 𝑀, 𝑤 |= execi (𝛼) iff 𝛼 ∈ 𝐸(𝑖, 𝑤) (t3) 𝑀, 𝑤 |= exec 𝐺 (𝛼) iff ∃𝑖 ∈ 𝐺 with 𝛼 ∈ 𝐸(𝑖, 𝑤) (t4) 𝑀, 𝑤 |= can_do 𝑖 (𝜑𝐴 ) iff 𝜑𝐴 ∈ 𝐴(𝑖, 𝑤) ∩ 𝐻(𝑖, 𝑤) (t5) 𝑀, 𝑤 |= can_do 𝐺 (𝜑𝐴 ) iff ∃𝑖 ∈ 𝐺 with 𝜑𝐴 ∈ 𝐴(𝑖, 𝑤) ∩ 𝐻(𝑖, 𝑤) (t6) 𝑀, 𝑤 |= pref _do 𝑖 (𝜑𝐴 , 𝑑) iff 𝜑𝐴 ∈ 𝐴(𝑖, 𝑤) and 𝑃 (𝑖, 𝑤, 𝜑𝐴 ) = 𝑑 (t7) 𝑀, 𝑤 |= pref _do 𝐺 (𝑖, 𝜑𝐴 ) iff 𝑀, 𝑤 |= pref _do 𝑖 (𝜑𝐴 , 𝑑) for 𝑑 = max{𝑃 (𝑗, 𝑤, 𝜑𝐴 ) | 𝑗 ∈ 𝐺 ∧ 𝜑𝐴 ∈ 𝐴(𝑗, 𝑤) ∩ 𝐻(𝑗, 𝑤)} (t8) 𝑀, 𝑤 |= ¬𝜙 iff 𝑀, 𝑤 ̸|= 𝜙 (t9) 𝑀, 𝑤 |= 𝜙 ∧ 𝜓 iff 𝑀, 𝑤 |= 𝜙 and 𝑀, 𝑤 |= 𝜓 (t10) 𝑀, 𝑤 |= B𝑖 𝜙 iff ||𝜙||𝑀 𝑖,𝑤 ∈ 𝑁 (𝑖, 𝑤) (t11) 𝑀, 𝑤 |= K𝑖 𝜙 iff 𝑀, 𝑣 |= 𝜙 for all 𝑣 ∈ 𝑅𝑖 (𝑤) As seen above, a physical action can be performed by a group of agents if at least one agent of the group can do it, and the level of preference for performing this action is set to the maximum among those of the agents enabled to do this action. For any inferential action 𝛼 performed by any agent 𝑖, we set: 𝑀, 𝑤 |= [𝐺 : 𝛼]𝜙 iff 𝑀 [𝐺:𝛼] , 𝑤 |= 𝜙 where 𝑀 [𝐺:𝛼] = ⟨𝑊, 𝑁 [𝐺:𝛼] , ℛ, 𝐸, 𝐵 [𝐺:𝛼] , 𝐶, 𝐴, 𝐻, 𝑃, 𝑉 ⟩, is the model representing the fact that the execution of an inferential action 𝛼 affects the sets of beliefs of agent 𝑖 and modifies the available budget. Such operation can add new beliefs by direct perception, by means of one inference step, or as a conjunction of previous beliefs. Hence, when introducing new beliefs (i.e., performing mental actions), the neighborhood must be extended accordingly. Notice that the execution of inferential actions only affects agents’ beliefs, i.e., the contents of their working memory. Mental actions have no effect on agents’ knowledge, which remains persistent. For details about belief/neighborhood update, we refer the reader to [16] where an axiomatiza- tion of the logic framework described so far is also provided, together with results concerning soundness and completeness of the logic. A key aspect in the definition of the logic is the following, which states under which conditions, and by which agent(s), an action may be performed. 𝐶(𝑗, 𝛼, 𝑤) enabled 𝑤 (𝐺, 𝛼) : ∃𝑗 ∈ 𝐺 (𝛼 ∈ 𝐸(𝑗, 𝑤) ∧ ≤ min 𝐵(ℎ, 𝑤)). |𝐺| ℎ∈𝐺 This condition states when an inferential action is enabled. In the above particular formulation (that is not fixed, but can be customized to the specific application domain) if at least an agent can perform it; and if the “payment” due by each agent, obtained by dividing the action’s cost equally among all agents of the group, is within each agent’s available budget. In case more than one agent in 𝐺 can execute an action, we implicitly assume the agent 𝑗 performing the action to be the one corresponding to the lowest possible cost. Namely, 𝑗 is such that 𝐶(𝑗, 𝛼, 𝑤) = minℎ∈𝐺 𝐶(ℎ, 𝛼, 𝑤). This definition reflects a parsimony criterion reasonably adoptable by cooperative agents sharing a crucial resource such as, e.g., energy or money. Other choices might be viable, so variations of this logic can be easily defined simply by devising some other enabling condition and, possibly, introducing differences in neighborhood update. Notice that the definition of the enabling function basically specifies the “concrete responsibility” that agents take while concurring with their own resources to actions’ execution. Also, in case of specification of various resources, different corresponding enabling functions might be defined. Our contribution to modularity is that functions 𝐴, 𝑃 and 𝐻, i.e., executability of physical actions, preference level of an agent about performing each action, and permission concerning which actions to actually perform, are not meant to be built-in. Rather, they can be defined via separate sub-theories, possibly defined using different logics, or, in a practical approach, even via pieces of code. This approach can be extended to function 𝐶, i.e., the cost of mental actions instead of being fixed may in principle vary, and be computed upon need. 3. Problem Specification and Inference: An Example, and Discussion In this section, we propose an example to explain the usefulness of this kind of logic underlying cognitive aspects; in fact, to the best of our knowledge, no one in literature is using logic in this way. For the sake of simplicity of illustration and of brevity, the example is in “skeletal” form. Consider a group of four agents, who are the crew of an ambulance, including a driver, two nurses, and a medical doctor. The driver is the only one enabled to drive the ambulance. The nurses are enabled to perform a number of tasks, such as, e.g., administer a pain reliever, or clean, disinfect and bandage a wound, measure vital signs. It is however the task of a doctor to make a diagnosis, to prescribe medications, to order, perform, and interpret diagnostic tests, and to perform complex medical procedures. Let us identify the four agents by integer numbers and, accordingly, let 𝐺 = {1, 2, 3, 4} be their group. Imagine that the hospital received notice of a car accident with an injured person. Then, it will inform the group of the fact that a patient needs help (how exactly is not treated here, because this depends on how the multi-agent system is implemented, but a message exchange will presumably suffice). The group will reason, and devise the intention/goal K𝑖 (intendG (rescue_patient)). Among the physical actions that agents in 𝐺 can perform, there are the following: diagnose_patient administer _urgent_treatment measure_vital _signs pneumothorax _aspiration local _anesthesia bandage_wounds drive_to_patient drive_to_hospital . The group will now be required to perform a planning activity. Assume that, as a result of the planning phase, the knowledge base of each agent 𝑖 contains the following rule, that specifies how to reach the intended goal in terms of actions to perform and sub-goals to achieve: (︀ K𝑖 intendG (rescue_patient) → intendG (drive_to_patient) ∧ intendG (diagnose_patient) ∧)︀ intendG (stabilize_patient) ∧ intendG (drive_to_hospital ) Thanks to the mentioned axiomatization for L-DINF (specifically, by axiom 18 in [16], stating that intendG (𝜑A ) ↔ ∀𝑖 ∈ 𝐺 intendi (𝜑A )) each agent has the specialized rule (for 𝑖 ≤ 4): (︀ K𝑖 intendG (rescue_patient) → intendi (drive_to_patient) ∧ intendi (diagnose_patient) ∧)︀ intendi (stabilize_patient) ∧ intendi (drive_to_hospital ) Therefore, the following is entailed for each agent: (︀ )︀ K𝑖 (︀intendi (rescue_patient) → intendi (drive_to_patient) )︀ K𝑖 (︀intendi (rescue_patient) → intendi (diagnose_patient))︀ K𝑖 (︀intendi (rescue_patient) → intendi (stabilize_patient) )︀ K𝑖 intendi (rescue_patient) → intendi (drive_to_hospital ) While driving to the patient and then going back to the hospital are actions, intendG (stabilize_patient) is a goal. Assume now that the knowledge base of each agent 𝑖 contains also the following general rules, stating that the group is available to perform each of the necessary actions. Which agent will in particular perform each action 𝜑𝐴 ? According to items (t4) and (t7) in the definition of truth values, for L-DINF formulas, this agent will be chosen as the one which best prefers to perform this action, among those that can do it. Formally, in the present situation, pref _doG (i , 𝜑A ) identifies an agent 𝑖 in the group with a maximum degree of preference on performing 𝜑𝐴 (any deterministic rule can be applied to select 𝑖 in case more agents express the highest degree), and can_doG (𝜑A ) is true if there is some agent 𝑖 in the group which is able and allowed to perform 𝜑𝐴 , i.e., 𝜑𝐴 ∈ 𝐴(𝑖, 𝑤) ∧ 𝜑𝐴 ∈ 𝐻(𝑖, 𝑤). (︀ K𝑖 intendG (drive_to_patient) ∧ can_doG (drive_to_patient)∧ )︀ (︀ pref _doG (i , drive_to_patient) → doG (drive_to_patient) K𝑖 intendG (diagnose_patient) ∧ can_doG (diagnose_patient)∧ )︀ (︀ pref _doG (i , diagnose_patient) → doG (diagnose_patient) K𝑖 intendG (drive_to_hospital ) ∧ can_doG (drive_to_hospital )∧ )︀ pref _doG (i , drive_to_hospital ) → doG (drive_to_hospital ) As before, such rules can be specialized to each single agent: (︀ K𝑖 intendi (drive_to_patient) ∧ can_doi (drive_to_patient) ∧ )︀ (︀ pref _doi (i , drive_to_patient) → doG (drive_to_patient) K𝑖 intendi (diagnose_patient) ∧ can_doi (diagnose_patient)∧ )︀ (︀ pref _doi (i , diagnose_patient) → doi (diagnose_patient) K𝑖 intendi (drive_to_hospital ) ∧ can_doi (drive_to_hospital )∧ )︀ pref _doi (i , drive_to_hospital ) → doi (drive_to_hospital ) So, for each action 𝜑𝐴 required by the plan, there will be some agent (let us assume for simplicity only one), for which doi (𝜑A ) will be concluded. In our case, the agent driver 𝑗 will conclude doj (drive_to_patient) and doj (drive_to_hospital ); the agent doctor ℓ will conclude doℓ (stabilize_patient). As previously stated, whenever an agent derives doi (𝜑A ) for any physical action 𝜑𝐴 , the action is supposed to have been performed via some kind of semantic attachment which links the agent to the external environment. Since intendG (stabilize_patient) is not an action but a sub-goal, the group will have to devise a plan to achieve it. This will imply sensing actions and forms of reasoning not shown here. Assume that the diagnosis has been pneumothorax, and that the patient has also some wounds which are bleeding. Upon completion of the planning phase, the knowledge base of each agent 𝑖 contains the following rule, that specifies how to reach the intended goal in terms of actions to be performed: (︀ K𝑖 intendG (stabilize_patient) → intendG (measure_vital _signs) ∧ intendG (local _anesthesia) ∧)︀ intendG (bandage_wounds) ∧ intendG (pneumothorax _aspiration) As before, these rules will be instantiated and elaborated by the single agents, and there will be some agent who will finally perform each action. Specifically, the doctor will be the one to perform pneumothorax aspiration, and the nurses (according to their competences and their preferences) will measure vital signs, administer local anesthesia and bandage the wounds. The new function 𝐻, in a sensitive domain such as healthcare, guarantees that each procedure is administered by one who is capable to (function 𝐴) but also enabled (function 𝐻), and so can take responsibility for the action. An interesting point concerns derogation, i.e., for instance, life or death situations where, unfortunately, no-one who is enabled to perform some urgently needed action is available; in such situations perhaps, anyone who is capable to perform this action might perform it. For instance, a nurse, in absence of a doctor, might attempt urgent pneumothorax aspiration. From such perspective, semantics could be modified as follows: (t4’) 𝑀, 𝑤 |= able_do 𝑖 (𝜑𝐴 ) iff 𝜑𝐴 ∈ 𝐴(𝑖, 𝑤) (t4”) 𝑀, 𝑤 |= enabled _do 𝑖 (𝜑𝐴 ) iff 𝜑𝐴 ∈ 𝐴(𝑖, 𝑤) ∩ 𝐻(𝑖, 𝑤) (t4-new) 𝑀, 𝑤 |= can_do 𝑖 (𝜑𝐴 ) iff (𝜑𝐴 ∈ 𝐴(𝑖, 𝑤) ∩ 𝐻(𝑖, 𝑤)) ∨ (𝜑𝐴 ∈ 𝐴(𝑖, 𝑤) ∧ ̸ ∃ 𝑗∈𝐺 : 𝜑𝐴 ∈ 𝐴(𝑗, 𝑤) ∩ 𝐻(𝑗, 𝑤)) (t5-new) 𝑀, 𝑤 |= can_do 𝐺 (𝜑𝐴 ) iff ∃ 𝑖 ∈ 𝐺 s.t. 𝑀, 𝑤 |= can_do 𝑖 (𝜑𝐴 ) Thanks to this example, the ductility of this approach and the importance that is given to the cognitive aspect of the agent is highlighted. 4. False-Beliefs: the “Sally-Anne” Task In approach proposed in [2], each agent has a version of the belief set of all the other agents. In such a proposal, belief sets are shared when agents belong to the same group, say 𝐺. But, as soon as an agent, say 𝑗, leaves the group 𝐺, its belief set might evolve and become different from the version owned by the other agents 𝑖 ∈ 𝐺. Sharing of belief sets, allows any agent 𝑖 in a group 𝐺 to perform inferences based on the beliefs of another agent ℎ ̸∈ 𝐺. Clearly, this is done w.r.t. the version of ℎ’s beliefs owned by 𝑖 (namely, the one shared the last time the two joined the same group). This means, agent 𝑖 might do some mental action impersonating ℎ, by exploiting its version of ℎ’s belief set and possibly updating such set. This extension of the logic framework is obtained by introducing modalities of the form B𝑖,𝑗 (in place of the B𝑖 described in Section 2.1). The rational is that the operator B𝑖,𝑗 is used to model the beliefs that agent 𝑖 has about 𝑗’s beliefs. This extension opens to the possibility that agents in 𝐺 infer false beliefs about ℎ. This may happen because agents 𝑖 ∈ 𝐺 are not aware of mental actions performed meanwhile by agents ℎ ̸∈ 𝐺. In this case, 𝑖’s version of the belief set of ℎ does not incorporate the last changes made by ℎ in its working memory. Consequently, all 𝑖 ∈ 𝐺 have an obsolete representation of ℎ’s beliefs. Note that all beliefs are shared among all members of a group 𝐺. To demonstrate that our logic is able to model relevant basic aspects of the Theory of Mind, we formalized the “Sally-Anne” task, an example of situation where false beliefs arise. The Sally–Anne test was introduced as a psychological test in developmental psychology in order to measure a person’s social cognitive ability to attribute false beliefs to others. The test was administered to children for the fist time in [17] and then in [18], to test their ability to develop a “Theory of Mind” concerning the expectation of how someone will act based on the awareness of that person’s false beliefs. The test has been then recently adopted to evaluate the cognitive capabilities of intelligent (possibly robotic) agents, see, e.g., [19]. The specification of the Sally-Anne task is the following: a child (or an agent), say Rose, is told a story about two girls, Sally and Anne, who are in a room with a basket and a box. In the story, Sally puts a doll into the basket, then leaves the room, and, in her absence, Anne moves the doll to the box. The child is then asked: “where does Sally believe the doll to be?”. To pass the test, the child should answer that Sally believes the doll to be in the basket. If asked for an explanation, she should answer that, since Sally did not see Anne moving the doll, she has the false belief that the doll is still in the basket. Our formalization of the task is found below. Notice that an uppercase initial letter denotes a variable symbol. The use of variables has however to be intended as a shorthand notation, as indeed, the language is propositional. We assume to have three agents, namely 1 (Sally), 2 (Anne), and 3 (observer). Initially, all agents belong to the same group and share the beliefs B𝑖,𝑗 (can_do 1 (𝑝𝑢𝑡𝐴 (𝑑𝑜𝑙𝑙, 𝑏𝑜𝑥))) and B𝑖,𝑗 (𝑖𝑛𝑡𝑒𝑛𝑑1 (𝑝𝑢𝑡𝐴 (𝑑𝑜𝑙𝑙, 𝑏𝑜𝑥))), for 𝑖, 𝑗 ∈ {1, 2, 3}, and that each agent has in her background knowledge the rule that states that an agent which is able and willing to perform some physical action will indeed do it: K𝑖 (can_do 𝑖 (Φ𝐴 ) ∧ 𝑖𝑛𝑡𝑒𝑛𝑑𝑖 (Φ𝐴 ) → do 𝑖 (Φ𝐴 )). It is easy to see that, by means of the mental actions, all the agents are able to derive do 1 (𝑝𝑢𝑡𝐴 (𝑑𝑜𝑙𝑙, 𝑏𝑜𝑥)) and, consequently, do 𝑃1 (𝑝𝑢𝑡𝐴 (𝑑𝑜𝑙𝑙, 𝑏𝑜𝑥)), which is the past event that records, in the agents’ memory, that the action has indeed been performed. For each 𝑖, there will also be the general knowledge about the affect of the physical action of moving/putting an object into a place, i.e., that the object will indeed be in that place: K𝑖 (do 𝑃𝑖 (𝑝𝑢𝑡𝐴 (𝑂𝑏𝑗, 𝑃 𝑙𝑎𝑐𝑒)) ∧ ¬do 𝑃𝑖 (𝑚𝑜𝑣𝑒𝐴 (𝑂𝑏𝑗, 𝑃 𝑙𝑎𝑐𝑒, 𝑃 𝑙𝑎𝑐𝑒1)) → in(𝑂𝑏𝑗, 𝑃 𝑙𝑎𝑐𝑒)) K𝑖 (do 𝑃𝑖 (𝑝𝑢𝑡𝐴 (𝑂𝑏𝑗, 𝑃 𝑙𝑎𝑐𝑒)) ∧ do 𝑃𝑖 (𝑚𝑜𝑣𝑒𝐴 (𝑂𝑏𝑗, 𝑃 𝑙𝑎𝑐𝑒, 𝑃 𝑙𝑎𝑐𝑒1)) → in(𝑂𝑏𝑗, 𝑃 𝑙𝑎𝑐𝑒1)) Therefore, for all agents (again by means of the mental actions that may exploit both knowledge and beliefs to infer new beliefs) we will easily have that B𝑖,𝑗 (𝑖𝑛(𝑑𝑜𝑙𝑙, 𝑏𝑜𝑥)) for 𝑖, 𝑗 = 1, 2, 3. Each agent 𝑖 of the group also has the knowledge describing the effects of leaving a room. We represent the fact that someone leaves the room as the execution of an action joinA , for an agent to join a new group. In this case, the new group will be newly formed, and will contain the agent alone (in general, an agent would be able to join any existing group, but in this example there is no other group to join): K𝑖 (can_do 𝑖 (joinA (𝑖, 𝑗)) ∧ intend 𝑖 (joinA (𝑖, 𝑗)) → do 𝑖 (joinA (𝑖, 𝑗))), This piece of knowledge states that any agent who can and wishes to leave the room/- group will do so. Thus, if we have (for each 𝑖) B𝑖,𝑖 (can_do 1 (joinA (1, 1))) and B𝑖,𝑖 (intend 1 (joinA (1, 1))), i.e., that Sally can and wants to leave the room, then all the agents conclude do 1 (joinA (1, 1)) and, consequently, do 𝑃1 (joinA (1, 1)). So, Sally is no longer in the group with agents 2 and 3. At this point therefore, agent 1 (Sally) is no longer able to observe what the others do. Let us assume, that agent 2 (Ann) acquires some other beliefs, possibly via interaction with the environment, of which Sally cannot be aware, being away from the group. Let us assume that the new beliefs are (for 𝑖 = 2, 3): B𝑖,𝑖 (can_do 2 (move 𝐴 (doll , box , basket))) and B𝑖,𝑖 (intend 2 (move 𝐴 (doll , box , basket))). From these beliefs and previous rules, via mental actions, agents 2 and 3 obtain do 2 (move 𝐴 (doll , box , basket)), do 𝑃2 (move 𝐴 (doll , box , basket)), and consequently, conclude that B𝑖,𝑗 (in(doll , basket)) for 𝑖, 𝑗 = 2, 3. Now, assume that we ask agent 3 (the observer) what agent 1 (Sally) would answer if asked where the doll is now. This accounts, for agent 3, to prove B3,1 (in(doll , Place)) for any constant replacing the variable Place (namely, to find a suitable instantiation of the variable Place to one between box and basket). So, agent 3 puts herself “in the shoes” of agent 1. This involves, for agent 3, “simulating” what agent 1 would be able to infer at this stage. The semantics for belief update that we introduced for B𝑖,𝑗 , applied here to B3,1 , makes agent 3 able to reason in agent 1’s neighborhood (i.e., within agent 1’s beliefs). So, 3 concludes immediately B3,1 (in(doll , box )). We have seen that agents 2 and 3 have instead concluded in(doll , basket), inference that agent 3 cannot do when she puts herself “in the shoes” of agent 1, which, having left the group, does not have the necessary beliefs available, which were formed after she left. So, translating the result in “human” terms, agent 3 is able to answer that agent 1 believes the doll to be (still) in the box. 5. Conclusions In this paper, we discussed cognitive aspects of an epistemic logic that we have proposed and developed to provide a way for a formal description of the cooperative activities of groups of agents. We have emphasized the importance of cognitive aspects, i.e.: having in the semantics particular functions that formalize the “way of thinking” of agents, and modelling the possibility for an agent to leave a group, thus losing the possibility, from then on, to be aware of the (changes in the) beliefs of its former group. We have shown how, in our logic, one can represent situations where the group’s behaviour can be customized according to the context at hand, and we have discussed how to solve the well-known Sally-Anne task. In past work, we have introduced the notion of canonical model of our logic, and we have performed the proof of strong completeness w.r.t. the proposed class of models (by means of a standard canonical-model argument). For lack of space we could not insert the proof in this paper, but we may note that it is very similar to that presented in [16]. The complexity of L-DINF is discussed in [16], which is the same as that of other similar logics. In future work, we mean to extend the formalization of group dynamics, e.g., to better model the evolution of the beliefs of an agent before joining a group, during the stay, after leaving, and (possibly) after re-joining. We also intend to incorporate (at least aspects of) our logic into the DALI language: this involves devising a user-friendly and DALI-like syntax, enhancing the language semantics, and extending the implementation. References [1] S. Costantini, V. Pitoni, Towards a logic of "inferable" for self-aware transparent logical agents, in: C. Musto, D. Magazzeni, S. Ruggieri, G. Semeraro (Eds.), Proceedings of XAI.it@AIxIA 2020, volume 2742 of CEUR Workshop Proceedings, CEUR-WS.org, 2020, pp. 68–79. URL: http://ceur-ws.org/Vol-2742/paper6.pdf. [2] S. Costantini, A. Formisano, V. Pitoni, An epistemic logic for formalizing group dynamics of agents, Submitted to a journal (2022). [3] A. I. Goldman, Theory of mind, in: E. Margolis, R. Samuels, S. P. Stich (Eds.), The Oxford Handbook of Philosophy of Cognitive Science, volume 1, Oxford University Press, 2012, pp. 402–424. doi:10.1093/oxfordhb/9780195309799.013.0017. [4] S. Costantini, Towards active logic programming, in: Online Proceedings of the 2nd Workshop on Component-based Software Development in Computational Logic, 1999. http://pages.di.unipi.it/brogi/ResearchActivity/COCL99/proceedings/index.html. [5] S. Costantini, A. Tocchio, A logic programming language for multi-agent systems, in: S. Flesca, S. Greco, N. Leone, G. Ianni (Eds.), Proc. of JELIA-02, volume 2424 of LNAI, Springer, 2002, pp. 1–13. doi:10.1007/3-540-45757-7_1. [6] S. Costantini, A. Tocchio, The DALI logic programming agent-oriented language, in: J. J. Alferes, J. A. Leite (Eds.), Proc. of JELIA-04, volume 3229 of LNAI, Springer, 2004, pp. 685–688. doi:10. 1007/978-3-540-30227-8_57. [7] G. De Gasperis, S. Costantini, G. Nazzicone, DALI multi agent systems framework, doi 10.5281/zen- odo.11042, DALI GitHub Software Repository, 2014. DALI: github.com/AAAI-DISIM-UnivAQ/ DALI. [8] S. Costantini, A. Tocchio, About declarative semantics of logic-based agent languages, in: M. Bal- doni, U. Endriss, A. Omicini, P. Torroni (Eds.), Declarative Agent Languages and Technologies III, volume 3904 of LNCS, Springer, 2005, pp. 106–123. doi:10.1007/11691792_7. [9] S. Costantini, G. De Gasperis, G. Nazzicone, DALI for cognitive robotics: Principles and prototype implementation, in: Y. Lierler, W. Taha (Eds.), Practical Aspects of Declarative Languages - 19th Int. Symp. PADL 2017, Proceedings, volume 10137 of LNCS, Springer, 2017, pp. 152–162. doi:10.1007/978-3-319-51676-9_10. [10] F. Aielli, D. Ancona, P. Caianiello, S. Costantini, G. De Gasperis, A. Di Marco, A. Ferrando, V. Mascardi, FRIENDLY & KIND with your health: Human-friendly knowledge-intensive dynamic systems for the e-health domain, in: J. B. et al. (Ed.), Highlights of Practical Applications of Scalable Multi-Agent Systems, volume 616 of Communications in Computer and Information Science, Springer, 2016, pp. 15–26. doi:10.1007/978-3-319-39387-2_2. [11] S. Costantini, L. De Lauretis, C. Ferri, J. Giancola, F. Persia, A smart health assistant via DALI logical agents, in: S. Monica, F. Bergenti (Eds.), Proc. of CILC 2021, volume 3002 of CEUR Workshop Proceedings, CEUR-WS.org, 2021, pp. 173–187. [12] S. Costantini, A. Formisano, V. Pitoni, An epistemic logic for multi-agent systems with budget and costs, in: W. Faber, G. Friedrich, M. Gebser, M. Morak (Eds.), Proc. of JELIA-21, volume 12678 of LNCS, Springer, 2021, pp. 101–115. doi:10.1007/978-3-030-75775-5_8. [13] A. S. Rao, M. P. Georgeff, Modeling rational agents within a BDI architecture, in: Proc. of the 2nd Int. Conf. on Principles of Knowledge Representation and Reasoning (KR’91), Morgan Kaufmann, 1991, pp. 473–484. ISBN:1-55860-165-1. [14] H. Van Ditmarsch, J. Y. Halpern, W. Van Der Hoek, B. Kooi, Handbook of Epistemic Logic, College Publications, 2015. ISBN:1-84890-158-5. [15] R. W. Weyhrauch, Prolegomena to a theory of mechanized formal reasoning, Artif. Intell. 13 (1980) 133–170. doi:10.1016/0004-3702(80)90015-6. [16] S. Costantini, A. Formisano, V. Pitoni, An epistemic logic for modular development of multi-agent systems, in: N. Alechina, M. Baldoni, B. Logan (Eds.), Engineering Multi-Agent Systems 9th International Workshop, EMAS 2021, Revised Selected papers, volume 13190 of LNCS, Springer, 2022, pp. 72–91. doi:10.1007/978-3-030-97457-2_5. [17] H. Wimmer, J. Perner, Beliefs about beliefs: Representation and constraining function of wrong beliefs in young children’s understanding of deception, Cognition 13 (1983) 103–128. doi:10. 1016/0010-0277. [18] S. Baron-Cohen, A. M.Leslie, U. Frith, Does the autistic child have a "theory of mind"?, Cognition 1 (1985) 37–46. doi:10.1016/0010-0277(85)90022-8. [19] L. Dissing, T. Bolander, Implementing theory of mind on a robot using dynamic epistemic logic, in: C. Bessiere (Ed.), Proc. of IJCAI 2020, ijcai.org, 2020, pp. 1615–1621. doi:10.24963/ijcai. 2020/224.