Intentional Reasoning as Non-monotonic Reasoning José Martı́n Castro-Manzano1 , Axel Arturo Barceló-Aspeitia1 , and Alejandro Guerra-Hernández2 1 Instituto de Investigaciones Filosóficas Universidad Nacional Autónoma de México Circuito Mario de la Cueva s/n Ciudad Universitaria, México, D.F., México, 04510 jmcmanzano@hotmail.com, abarcelo@minerva.filosoficas.unam.mx 2 Departamento de Inteligencia Artificial Universidad Veracruzana Sebastián Camacho No. 5, Xalapa, Ver., México, 91000 aguerra@uv.mx Abstract. Intentional reasoning is also logical reasoning. Since it is a dynamic process that involves reasoning from beliefs, goals and time, it requires both a temporal semantics and a non-monotonic behavior. In this work we propose a model of intentional reasoning as a case of non- monotonic reasoning. We also show the consistency and soundness of the system. Keywords: Defeasible logic, temporal logic, BDI logic. 1 Introduction Intentional reasoning is also a form of logical reasoning. Moreover, it is a dynamic process that uses beliefs and intentions, but also time. It has been mainly mod- eled via BDI logics, for instance [18,20,22]; however, there are two fundamental problems with such approaches: in first place, human reasoning is not and should not be monotonic [15], and thus, the logical models should be non-monotonic; and in second place, intentional states should respect temporal norms, and so, the logical models need to be temporal as well. Thereby, the proof process of intentional reasoning has to have some sort of control over time and has to take into account a form of non-monotonic inference using beliefs and intentions. In the current picture defeasible logics have been mainly developed to rea- son about beliefs [17] but have been barely used to reason about temporal structures [11]; on the other hand, intentional logics have been mostly used to reason about intentional states and temporal behavior but most of them are monotonic. In this work we propose intentional reasoning as a particular case of non-monotonic reasoning. And in order to solve the double problem we mentioned above, our main contribution is the adaptation and extension for CT LAgentSpeak(L) [13] semantics with a non-monotonic framework. So, a defea- sible temporal logic that deals with the non-monotonicity of intentions while 23 taking care of temporal structures is proposed. We also show the consistency and soundness of the system. In Section 2 we discuss the case of intentional reasoning as non-monotonic reasoning and we expose a non-monotonic framework for intentional reasoning in Section 3. In Section 4 we display the system, its consistency and soundness. Finally, in Section 5 we discuss the results and we mention future work. 2 Intentional reasoning is non-monotonic reasoning The BDI models based upon Bratman’s theory [4] tend to interpret intentions as a unique fragment [18,20,22] while Bratman’s richer framework distinguished three classes of intentions: deliverative, non-deliverative and policy-based. In particular, policy-based intentions are of great importance given their structure and behavior: they have the form of rules and behave like plans. These remarks are relevant because the existing formalisms, despite of recognizing the intimate relationship between plans and intentions, seem to forget that intentions behave like plans. As Bratman has argued, plans are intentions as well [4]. In this way we can set policy-based intentions to be structures te : ctx ← body [2] (see Table 1). Now, consider the next example for sake of argument: on(X, Y ) ← put(X, Y ). This intention tells us that, for an agent to achieve on(a, b), it typically has to put a on b. If we imagine such an agent is immersed in a dynamic environment, of course the agent will try to put, typically, a on b; nevertheless, a rational agent would only do it as long as it is possible. Therefore, it results quite natural to talk about some intentions that are maintained typically but not absolutely. And so, it is reasonable to conclude that intentions, and particularly policy-based, allow defeasible intentional rea- soning [10]. However, the current BDI models are monotonic and non-monotonic logics are barely used to reason about time [11] or intentional states. Thus, a de- feasible temporal logic that deals with the non-monotonicity of intentions while taking care of temporal structures has not been developed yet. Thus, for example, standard First Order Logic is an instance of monotonic atemporal reasoning; default logic [19] is an instance of non-monotonic atemporal reasoning. In turn, BDI logic [18,20,22] is an example of temporal but monotonic reasoning. Our proposal is a case of temporal and non-monotonic reasoning. Traditional BDI models [5,6,14,18,20,22] formalize intentional reasoning in a monotonic way, while our proposal aims to do it non-monotonically. This is not only needed, it is also justified since intentions imply pro-activity, inertia (once an intention has been taken, it resists being abandoned) and admissibil- ity (once an intention has been taken, the agent will not consider contradictory options). Therefore intentions and intentional reasoning require a notion of com- mitment (given the principle of pro-activity), a notion of consistency (given the admissibility criteria) and a notion of retractability (given the notion of inertia). These features guarantee, respectively, that intentions need mechanisms of com- mitment, defeasibility and consistency which, in turn, allow the research about 24 intentions in terms of revision or non-monotonicity: just as the changes of beliefs require a theory of belief revision [1] or a non-monotonic logic [17], the changes of intentions require a theory of intention revision or a non-monotonic logic of intention. 3 Non-monotonic framework Despite enormous avances in this area, if we take into account the philosophical foundations of rational agency [4], it is not hard to see that most BDI logics fail to grasp all the properties of intentions: functional properties like proactiv- ity, admissibility and inertia; descriptive properties like partiality, hierarchy and dynamism; and of course, the normative properties: internal consistency, strong consistency and means-end coherence. The explanation of these properties can be found in [4]. Following these ideas we propose the next framework: Definition 1 (Non-monotonic intentional framework) A non-monotonic inten- tional framework is a tuple B, I, FB , FI , , |∼ , , ∼| ,  where: – B denotes the belief base. – I denotes the set of intentions. – FB ⊆ B denotes the basic beliefs. – FI ⊆ I denotes the basic intentions. –  and  are strong consequence relations. – |∼ and ∼| are weak consequence relations. – ⊆ I 2 s.t.  is acyclic. With the help of this framework we can start to represent the non-monotonic nature of intentional reasoning. We assume a commitment strategy embedded in the agent architecture, i.e, we assume the inertia of intentions by a fixed mechanism that is single-minded, because if there is no commitment or the agent is blindly-committed, there is no sense in talking about inertia [12,13], i.e., in reconsidering intentions. As usual, B denotes the beliefs base, which are literals. FB stands for the beliefs that are considered basic; and similarly FI stands for intentions considered as basic. Each intention φ ∈ I is a structure te : ctx ← body where te represents the goal of the intention –so we preserve proactivity–, ctx a context and the rest denotes the body. When ctx or body are empty we write te : ← or just te. We also preserve internal consistency by allowing the context of an intention, ctx(φ), ctx(φ) ∈ B and by letting te be the head of the intention. So, strong consistency is implied by internal consistency (given that strong consistency is ctx(φ) ∈ B). Means-end coherence is implied by admissibility and the hierarchy of intentions is represented by the order relation, which we require to be acyclic in order to solve conflicts between intentions. Again, all these features can be found in [4]. And with this framework we can arrange a notion of inference where we say that φ is strongly (weakly) derivable from a sequence ∆ iff there is a proof of ∆  φ (∆ |∼ φ). And also, that φ is not strongly (weakly) provable iff there is a proof of ∆  φ (∆ ∼| φ), where ∆ = B, I. 25 4 N CT LAgentSpeak(L) As we said above different logics have been proposed to characterize the ratio- nal behavior of agents. The most common logics are BDI systems [18,20,22] in which the behavior of the agents is specified in terms of changes in their mental states. These logics are used to reason about rational agents, but are not used to program them. We also have programming languages that have been proposed to reduce the gap between the theory (the logical specification) and the practice (the implementation). In this work we adopt AgentSpeak(L) [18] because it has a well defined operational semantics. The problem, however, is that these partic- ular semantics exclude modalities which are important to represent intentional states. To avoid this problem we use CT LAgentSpeak(L) [13] as a logical tool for the formal specification. Of course, initially, the approach is similar to a BDI CT L system defined after B KD45 DKD I KD with the temporal operators: next ( ), eventually (♦), always (), until (U), optional (E), inevitable (A), and so on, defined after CT L∗ [7,9]. In this section we are going to expose the syntax and semantics of CT LAgentSpeak(L) . 4.1 Syntax of AgentSpeak(L) An agent ag is formed by a set of plans ps and beliefs bs (grounded literals). Each plan has the form te : ctx ← h. The context ctx of a plan is a literal or a conjunction of them. A non empty plan body h is a finite sequence of actions A(t1 , . . . , tn ), goals g (achieve ! or test ? an atomic formula P (t1 , . . . , tn )), or beliefs updates u (addition + or deletion −). denotes empty elements, e.g., plan bodies, contexts, intentions. The trigger events te are updates (addition or deletion) of beliefs or goals. The syntax is shown in Table 1. ag ::= bs ps h ::= h1 ;  |  bs ::= b1 . . . bn (n ≥ 0) h1 ::= a | g | u | h1 ; h1 ps ::= p1 . . . pn (n ≥ 1) at ::= P (t1 , . . . , tn ) (n ≥ 0) p ::= te : ctx ← h a ::= A(t1 , . . . , tn ) (n ≥ 0) te ::= +at | − at | + g | − g g ::= !at | ?at ctx ::= ctx1 |  u ::= +b | − b ctx1 ::= at | ¬at | ctx1 ∧ ctx1 Table 1. Sintax of AgentSpeak(L) adapted from [2]. 4.2 Semantics of AgentSpeak(L) The operational semantics of AgentSpeak(L) are defined by a transition system, as showed in Figure 1, between configurations ag, C, M, T, s, where: 26 Rel2 SelEv SelEv1 RelPl Rel1 ApplPl SelEv2 ProcMsg Appl2 Appl1 ClrInt1 SelInt2 AchvGl ClrInt3 ClrInt2 SelInt SelAppl ClrInt SelAppl SelInt1 ExtEv TestGl1 AddBel Action IntEv TestGl2 DelBel ExecInt AddIM Fig. 1. The interpreter for AgentSpeak(L) as a transition system. – ag is an agent program formed by beliefs bs and plans ps. – An agent circumstance C is a tuple I, E, A where I is the set of intentions {i, i , . . . , n} s.t. i ∈ I is a stack of partially instantiated plans p ∈ ps; E is a set of events {te, i , te , i  , . . . , n}, s.t. te is a triggerEvent and each i is an intention (internal event) or an empty intention (external event); and A is a set of actions to be performed by the agent in the environment. – M is a tuple In, Out, SI that works as a mailbox, where In is the mailbox of the agent, Out is a list of messages to be delivered by the agent and SI is a register of suspended intentions (intentions that wait for an answer message). – T is a tuple R, Ap, ι, , ρ that registers temporal information: R is the set of relevant plans given certain triggerEvent; Ap is the set of applicable plans (the subset of R s.t. bs |= ctx); ι,  and ρ register, respectively, the intention, the event and the current plan during an agent execution. – The label s ∈ {SelEv, RelP l, AppP l, SelAppl, SelInt, AddIM, ExecInt, ClrInt, P rocM sg} indicates the current step in the reasoning cycle of the agent. Under such semantics a run is a set Run = {(σi , σj )|Γ  σi → σj } where Γ is the transition system defined by AgentSpeak(L) operational semantics and σi , σj are agent configurations. CT L 4.3 Syntax of BDIAS(L) CT LAgentSpeak(L) may be seen as an instance of BDI CT L . Similar approaches have been accomplished for other programming languages [8]. The idea is to define some BDI CT L semantics in terms of AgentSpeak(L) structures. So, we need a language able to express temporal and intentional states. Thus, we require in first place some way to express these features. 27 CT L Definition 2 (Syntax of BDIAS(L) ) If φ is an AgentSpeak(L) atomic formula, CT L then BEL(φ), DES(φ) and INT(φ) are well formed formulas of BDIAS(L) . To specify the temporal behavior we use CT L∗ in the next way. CT L CT L Definition 3 (BDIAS(L) temporal syntax) Every BDIAS(L) formula is a state formula s: – s ::= φ|s ∧ s|¬s – p ::= s|¬p|p ∧ p|Ep|Ap| p|♦p|p|p U p CT L 4.4 Semantics of BDIAS(L) Initially the semantics of BEL, DES and INT is adopted from [3]. So, we use the next function: agoals( ) = {}, {at} ∪ agoals(i) if p = +!at : ct ← h, agoals(i[p]) = agoals(i) otherwise which gives us the set of atomic formulas (at) attached to an achievement goal (+!) and i[p] denotes the stack of intentions with p at the top. CT L Definition 4 (BDIAS(L) semantics) The operators BEL, DES and INT are de- fined in terms of an agent ag and its configuration ag, C, M, T, s: BELag,C,M,T,s (φ) ≡ φ ∈ bs   INTag,C,M,T,s (φ) ≡ φ ∈ agoals(i) ∨ agoals(i) i∈CI te,i∈CE DESag,C,M,T,s (φ) ≡ +!φ, i ∈ CE ∨ INT(φ) where CI denotes current intentions and CE suspended intentions. CT L 4.5 The system N BDIAS(L) By now we have a defeasible framework for intentions that lacks temporal repre- sentation; while the BDI temporal model described before grasps the temporal representation but lacks non-monotonicity. The next step is the proposal of a system denoted by N BDI because it has a non-monotonic behavior. An inten- CT L tion φ in N BDIAS(L) is of course a structure g : ctx ← body where g is the head, ctx is the context and body is the body of the rule. We will denote an intention φ with head g by φ[g]. Also, a negative intention is denoted by φ[g c ], i.e., the intention φ with ¬g as the head. The semantics of this theory will require a Kripke structure K = S, R, V  where S is the set of agent configurations, R is an access relation defined after the transition system Γ and V is a valuation function that goes from agent configurations to true propositions in those states. 28 Definition 5 Let K = S, Γ, V , then: – S is a set of agent configurations c = ag, C, M, T, s. – Γ ⊆ S 2 is a total relation such that for all c ∈ Γ there is a c ∈ Γ s.t. (c, c ) ∈ Γ . – V is valuation s.t.: - VBEL (c, φ) = BELc (φ) where c = ag, C, M, T, s. - VDES (c, φ) = DESc (φ) where c = ag, C, M, T, s. - VINT (c, φ) = INTc (φ) where c = ag, C, M, T, s. – Paths are sequences of configurations c0 , . . . , cn s.t. ∀i(ci , ci+1 ) ∈ R. We use xi to indicate the i-th state of path x. Then: S1 K, c |= BEL(φ) ⇔ φ ∈ VBEL (c) S2 K, c |= DES(φ) ⇔ φ ∈ VDES (c) S3 K, c |= INT(φ) ⇔ φ ∈ VINT (c) S4 K, c |= Eφ ⇔ ∃x = c1 , . . . ∈ K|K, x |= φ S5 K, c |= Aφ ⇔ ∀x = c1 , . . . ∈ K|K, x |= φ P1 K, c |= φ ⇔ K, x0 |= φ where φ is a state formula. P2 K, c |= φ ⇔ K, x1 |= φ. P3 K, c |= ♦φ ⇔ K, xn |= φ for n ≥ 0 P4 K, c |= φ ⇔ K, xn |= φ for all n P5 K, c |= φ U ψ ⇔ ∃k ≥ 0 s.t. K, xk |= ψ and for all j, k, 0 ≤ j < k|K, cj |= φ or ∀j ≥ 0 : K, xj |= φ As we saw in Section 3, we have four cases of proof: if the sequence is ∆  φ, we say φ is strongly provable; if it is ∆  φ we say φ is not strongly provable. If is ∆ |∼ φ we say φ is weakly provable and if it is ∆ ∼| φ, then φ is not weakly provable. Definition 6 (Proof ) A proof of φ from ∆ is a finite sequence of beliefs and intentions satisfying: 1. ∆  φ iff 1.1. A(INT(φ)) or 1.2. A(∃φ[g] ∈ FI : BEL(ctx(φ)) ∧ ∀ψ[g  ] ∈ body(φ)  ψ[g  ]) 2. ∆ |∼ φ iff 2.1. ∆  φ or 2.2. ∆  ¬φ and 2.2.1. ♦E(INT(φ) U ¬BEL(ctx(φ))) or 2.2.2. ♦E(∃φ[g] ∈ I : BEL(ctx(φ)) ∧ ∀ψ[g  ] ∈ body(φ) |∼ ψ[g  ]) and 2.2.2.1. ∀γ[g c ] ∈ I, γ[g c ] fails at ∆ or 2.2.2.2. ψ[g  ]  γ[g c ] 3. ∆  φ iff 3.1. ♦E(INT(¬φ)) and 3.2. ♦E(∀φ[g] ∈ FI : ¬BEL(ctx(φ)) ∨ ∃ψ[g  ] ∈ body(φ)  ψ) 4. ∆ ∼| φ iff 4.1. ∆  φ and 4.2. ∆  ¬φ or 4.2.1. A¬(INT(φ) U ¬BEL(ctx(φ))) and 4.2.2. A(∀φ[g c ] ∈ I : ¬BEL(ctx(φ)) ∨ ∃ψ[g  ] ∈ body(φ) ∼| ψ[g  ]) or 4.2.2.1. ∃γ[g c ] ∈ I s.t. γ[g c ] succeds at ∆ and 4.2.2.2. ψ[g  ]  γ[g c ] 29 4.6 Consistency Now we suggest a square of opposition in order to describe some desired prop- erties of the system. Proposition 1 (Subalterns1 ) If  φ then |∼ φ. Proof. Let us assume that  φ but not |∼ φ, i.e., ∼| φ. Then, given  φ we have two general cases. Case 1: given the initial assumption that  φ, by Definition 6 item 1.1, we have that A(INT(φ)). Now, given the second assumption, i.e., that ∼| φ, by Definition 6 item 4.1, we have  φ. And so, ♦E(INT(¬φ)), and thus, by the temporal semantics, we get ¬φ; however, given the initial assumption, we also obtain φ, which is a contradiction. Case 2: given the assumption that  φ, by Definition 6 item 1.2, we have that ∃φ[g] ∈ FI : BEL(ctx(φ)) ∧ ∀ψ[g  ] ∈ body(φ)  ψ[g  ]. Now, given the second assumption, that ∼| φ, we also have  φ and so we obtain ♦E(∀φ[g] ∈ FI : ¬BEL(ctx(φ)) ∨ ∃ψ[g  ] ∈ body(φ)  ψ), and thus we can obtain ∀φ[g] ∈ FI : ¬BEL(ctx(φ)) ∨ ∃ψ[g  ] ∈ body(φ)  ψ) which is ¬(∃φ[g] ∈ FI : BEL(ctx(φ)) ∧ ∀ψ[g  ] ∈ body(φ)  ψ[g  ]).  Corollary 1 (Subalterns2 ) If ∼| φ then  φ. Proposition 2 (Contradictories1 ) There is no φ s.t.  φ and  φ. Proof. Assume that there is a φ s.t.  φ and  φ. If  φ then, by Definition 6 item 3.1, ♦E(INT(¬φ)). Thus, by proper semantics, we can obtain ¬φ. However, given that  φ it also follows that φ, which is a contradiction.  Corollary 2 (Contradictories2 ) There is no φ s.t. |∼ φ and ∼| φ. Proposition 3 (Contraries) There is no φ s.t.  φ and ∼| φ. Proof. Assume there is a φ such that  φ and ∼| φ. By Proposition 1, it follows that |∼ φ, but that contradicts the assumption that ∼| φ by Corollary 2.  Proposition 4 (Subcontraries) For all φ either |∼ φ or  φ. Proof. Assume it is not the case that for all φ either |∼ φ or  φ. Then there is φ s.t. ∼| φ and  φ. Taking ∼| φ it follows from Corollary 1 that  φ. By Proposition 2 we get a contradiction with  φ.  So, gathering the results, we get the next square of opposition where c denotes contradictories, s subalterns, k contraries and r subcontraries. φ< k > ∼| φ < > ∨ ∨ s c s ∨ < > ∨ |∼ φ < r >φ 30 Corollary 3 (Coherence) If  φ then it is false that  φ. And if If ∼| φ then it is false that |∼ φ. Proposition 1 and Corollary 1 represent supraclassicality; Proposition 2 and Corollary 2 stand for consistency while the remaining statements specify the coherence of the square, and thus, the overall coherence of the system. 4.7 Soundness Now, the idea is to show the framework is sound with respect to its semantics. Thus, as usual, we will need some notions of satisfaction and validity. Definition 7 (Satisfaction) A formula φ is true in K iff φ is true in all config- urations σ in K. This is to say, K |= φ ⇔ K, σ |= φ for all σ ∈ S. Definition 8 (Run of an agent in a model) Given  an initial  configuration β, a β β β transition system Γ and a valuation V , KΓ = SΓ , RΓ , V denotes a run of an agent in a model. CT L Definition 9 (Validity) A formula φ ∈ BDIAS(L) is true for any agent run in Γ iff ∀KΓβ |= φ Further, we will denote (∃KΓβ |= φ U ¬BEL(ctx(φ)))∨ |= φ by |≈ φ. We can observe, moreover, that |= φ ≥ |≈ φ and ≈| φ ≥ =| φ. With these remarks we should find a series of translations s.t.: φ > ∀KΓβ |= φ > |= φ > ∨ |∼ φ > |≈ φ Proposition 5 The following relations hold: a)  φ implies |= φ b) |∼ φ implies |≈ φ Proof. Base case. Taking ∆i as a sequence with i = 1, we have two basic cases. Case a) If we assume  φ, we have two subcases. First subcase is given by Def- inition 6 item 1.1. Thus we have A(INT(φ)). This means, by Definition 5 items P4 and S5 and Definition 4, that for all paths and all states φ ∈ CI ∨ CE . We can represent this expression, by way of a translation, in terms of runs. Since paths and states are sequences of agent configurations we have that ∀KΓβ |= φ, which implies |= φ. Second subcase is given by Definition 6 item 1.2, which in terms of runs means that for all runs ∃φ[g] ∈ FI : BEL(ctx(φ)) ∧ ∀ψ[g  ] ∈ body(φ)  ψ[g  ]. Since ∆1 is a single step, body(φ) = and for all runs BEL(ctx(φ))), ctx(φ) ∈ FB . Then ∀KΓβ |= φ which, same as above, implies |= φ. 31 Case b) Let us suppose |∼ φ. Then we have two subcases. The first one is given by Definition 6 item 2.1. So, we have that  φ which, as we showed above, already implies |= φ. On the other hand, by item 2.2, we have  ¬φ and two alternatives. The first alternative, item 2.2.1, is ♦E(INT(φ) U ¬BEL(ctx(φ))). Thus, we can reduce this expression by way of Definition 5 items P3 and S4, to a translation in terms of runs: ∃KΓβ |= φ U ¬BEL(ctx(φ)), which implies |≈ φ. The second alternative comes from item 2.2.2, ♦E(∃φ[g] ∈ I : BEL(ctx(φ)) ∧ ∀ψ[g  ] ∈ body(φ) |∼ ψ[g  ]) which in terms of runs means that for some run ∃φ[g] ∈ I : BEL(ctx(φ)) ∧ ∀ψ[g  ] ∈ body(φ) |∼ ψ[g  ], but ∆1 is a single step, and thus body(φ) = . Thus, there is a run in which ∃φ[g] ∈ I : BEL(ctx(φ)), i.e., (∃KΓβ |= (φ U ¬BEL(ctx(φ))) by using the weak case of Definition 6 P5. Thus, by addition, (∃KΓβ |= (φ U ¬BEL(ctx(φ)))∨ |= φ, and therefore, |≈ φ. Inductive case. Case a) Let us assume that for n ≤ k, if ∆n  φ then ∆ |= φ. And suppose ∆n+1 . Further, suppose ∆n  φ, then we have two alternatives. First one being, by Definition 6 item 1.1, that we have an intention φ s.t. ctx(φ) = body(φ) = . Since body(φ) is empty, it trivially holds at n, and by the induction hypothesis, body(φ) ⊆ ∆n+1 , and thus |= φ. Secondly, by Definition 6 item 1.2, for all runs ∃φ[g] ∈ I : BEL(ctx(φ)) ∧ ∀ψ[g  ] ∈ body(φ)  ψ[g  ]. Thus, for all runs n, ∀ψ[g  ] ∈ body(φ)  ψ[g  ], and so by the induction hypothesis, body(φ) ⊆ ∆n+1 , i.e., ∆  ψ[g  ]. Therefore, |= φ. Case b) Let us assume that for n ≤ k, if ∆n |∼ φ then ∆ |≈ φ. And suppose ∆n+1 . Assume ∆n |∼ φ. We have two alternatives. The first one is given by Definition 6 item 2.1, i.e.,  φ, which already implies |= φ. The second alternative is given by item 2.2, ∆  ¬φ and two subcases: ♦E(INT(φ) U ¬BEL(ctx(φ))) or ♦E(∃φ[g] ∈ I : BEL(ctx(φ)) ∧ ∀ψ[g  ] ∈ body(φ) |∼ ψ[g  ]). If we consider the first subcase there are runs n which comply with the definition of |≈ φ. In the remaining subcase we have ∀ψ[g  ] ∈ body(φ) |∼ ψ[g  ], since body(φ) ⊆ ∆n , by the induction hypothesis ∆ |∼ ψ[g  ], and thus, ∆n+1 |∼ φ, i.e., |≈ φ.  Moreover, we can find a series of translations for the remaining fragments: ∼| φ > ∃KΓβ |= ¬φ ∧ ∀KΓβ |= ¬(φ U ¬BEL(ctx(φ))) > ≈| φ ∨ > φ > =| φ Proposition 6 The following relations hold: a)  φ implies =| φ b) ∼| φ implies ≈| φ Proof. Base case. Taking ∆i as a sequence with i = 1, we have two basic cases. Case a) If we assume  φ, by Definition 6 item 3.1, we have ♦E(INT(¬φ)). Since ∆1 is a single step, already we have its translation ∃KΓβ |= ¬φ, which implies =| φ. Case b) Let us suppose ∼| φ. By Definition 6 item 4.1 we can a use the single condition  φ, but as we showed above,  φ has a translation ∃KΓβ |= ¬φ; 32 and by item 4.2.1 A¬(INT(φ) U ¬BEL(ctx(φ))), which in terms of runs means ∀KΓβ |= ¬(φ U ¬BEL(ctx(φ))). Thus, by conjunction of these last translations, ≈| φ. Inductive case. Case a) Let us assume that for n ≤ k, if ∆n  φ then ∆ =| φ. And suppose ∆n+1 . Take ∆n  φ. By Definition 6 item 3.2, we have ♦E(INT(¬φ)), which can be translated directly to a run of size n s.t. ∃KΓβ |= ¬φ, and by the induction hypothesis, body(φ) ⊆ ∆n+1 , and thus =| φ. Case b) Let us consider that for n ≤ k, if ∆n ∼| φ then ∆ ≈| φ. And suppose ∆n+1 . Let us suppose ∼| φ. By Definition 6 item 4.1 we can a use the single condition  φ, and as we showed above, it has a translation ∃KΓβ |= ¬φ. Further, by Definition 6 item 4.2 and 4.2.1 we can extract, respectively, ∆n |= ¬φ and A¬(INT(φ) U ¬BEL(ctx(φ))), i.e., for ∆n , ∀KΓβ |= ¬(φ U ¬BEL(ctx(φ))). Thus, by the induction hypothesis and by conjunction of these last translations, ∆n+1 ∼| φ, thus, ≈| φ.  5 Conclusion We proposed a logic to deal with the non-monotonicity of intentional reasoning while taking care of temporal structures. We were able to do this by extending a defeasible framework with some temporal semantics. Then we observed the system preserves supraclassicality, consistency and soundness. The relevance of this work becomes clear once we notice that, although intentions have received a lot of attention, their dynamic features have not been studied completely [21]. There are formal theories of intentional reason- ing [5,6,14,18,20,22] but very few of them consider the revision of intentions [21] or the non-monotonicity of intentions [10] as legitimate research topics, which we find odd since the foundational theory guarantees that such research is le- gitimate and necessary [4]. Recent works confirm the status of this emerging area [10,21,16]. Finally, as part of our current work, we are trying to find relations between the notion of inference of this system and a notion of revision. Plus, since our model is related to AgentSpeak(L), an implementation may follow organically. Acknowledgements. The authors would like to thank the anonymous review- ers for their useful comments and precise corrections. The first author is sup- ported by the CONACyT scholarship 214783. References 1. Alchourrón, C. E., Gärdenfors, P., Makinson, D.: On the logic of theory change: Partial meet contraction and revision functions. Journal of Symbolic Logic (1985) 50 510–530 2. Bordini, R.H., Wooldridge, M., Hübner, J.F.: Programming Multi-Agent Systems in AgentSpeak using Jason (Wiley Series in Agent Technology). John Wiley & Sons (2007) 33 3. Bordini, R.H., Moreira, Á.F.: Proving BDI Properties of Agent-Oriented Program- ming Languages. Annals of Mathematics and Artificial Intelligence (2004) 42 197– 226 4. Bratman, M.E.: Intention, Plans, and Practical Reason. Cambridge University Press (1999) 5. Chen, X, Liu, G.: A logic of intention. Proceedings of the 16th international joint conference on Artifical intelligence (1999) 1 172–177 6. Cohen, P., Levesque, H.: Intention is choice with commitment. Art. Int. (1990) 42(3), 213-261 7. Clarke, E.M. Jr., Grumberg, O.,Peled. D.A.: Model Checking. MIT Press (1999). 8. Dastani, M., van Riemsdijk, M.B., Meyer, J.C.: A grounded specification language for agent programs. Proceedings of the 6th international joint conference on Au- tonomous agents and multiagent systems ’07 AAMAS ’07 (2007) 1–8 9. Emerson, A.: Temporal and modal logic. Handbook of Theoretical Computer Sci- ence, Elsevier Science Publishers (1995) 995–1072 10. Governatori, G., Padmanabhan, V. and Sattar, A.: A Defeasible Logic of Policy- based Intentions. Proceedings of the 15th Australian Joint Conference on Artificial Intelligence: Advances in Artificial Intelligence. LNAI-2557, Springer Verlag (2002) 11. Governatori, G., Terenziani, P.: Temporal Extensions to Defeasible Logic. Proceed- ings of the 20th Australian joint conference on Advances in artificial intelligence (2007) 476–485 12. Guerra-Hernández, A., Castro-Manzano, J.M., El-Fallah-Seghrouchni, A.: Toward an AgentSpeak(L) Theory of Commitment and Intentional Learning. Proceedings of the 7th Mexican International Conference on Artificial Intelligence: Advances in Artificial Intelligence MICAI 2008, LNCS, vol. 5317, 848–858, Springer-Verlag, Berlin Heidelberg, (2008) 13. Guerra-Hernández, A., Castro-Manzano, J.M., El-Fallah-Seghrouchni, A.: CTL AgentSpeak(L): a Specification Language for Agent Programs. J. Algorithms (2009) 64(1) 31–40 14. Konolige, K., Pollack, M. E.: A representationalist theory of intentions. Proceed- ings of International Joint Conference on Artificial Intelligence (IJCAI-93) (1993) 390–395 15. Nute, D.: Defeasible logic. INAP 2001, LNAI 2543M, Springer-Verlag, (2003) 151- 169 16. Icard, Th., Pacuit. E., Shoham, Y.: Joint revision of belief and intention. Pro- ceedings of the Twelfth International Conference on the Principles of Knowledge Representation and Reasoning, (2010) 17. Prakken, H., Vreeswijk, G.: Logics for defeasible argumentation. In D. Gabbay and F. Guenthner (eds.), Handbook of Philosophical Logic, second edition, Vol 4, Kluwer Academic Publishers (2002) 219-318 18. Rao, A.S.: AgentSpeak(L): BDI agents speak out in a logical computable language. In: de Velde, W.V., Perram, J.W. (eds.) MAAMAW. LNCS, vol. 1038, Springer, Heidelberg (1996) 42–55 19. Reiter, R.: A logic for default reasoning. Artificial Intelligence, (1980) 13 81-132 20. Singh, M.P., Rao, A.S., Georgeff, M.P.: Formal Methods in DAI: Logic-Based Rep- resentation and Reasoning. In: Multiagent Systems: A Modern Approach to Dis- tributed Artificial Intelligence, MIT Press, Cambridge (1999) 331–376 21. van der Hoek, W., Jamroga, W., Wooldridge, M.: Towards a theory of intention revision. Synthese (2007) 155(2) 265–290 22. Wooldridge, M.: Reasoning about Rational Agents. MIT Press (2000) 34