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 nonmonotonic reasoning. We also show the consistency and soundness of the system.
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
modeled via BDI logics, for instance [
In the current picture defeasible logics have been mainly developed to
reason about beliefs [
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 [
As Bratman has argued, plans are intentions as well [
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
reasoning [
Thus, for example, standard First Order Logic is an instance of monotonic
atemporal reasoning; default logic [
Traditional BDI models [
Despite enormous avances in this area, if we take into account the philosophical
foundations of rational agency [
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 [
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 [
N CT LAgentSpeak(L) semantics of CT LAgentSpeak(L).
As we said above different logics have been proposed to characterize the
rational behavior of agents. The most common logics are BDI systems [
To avoid this problem we use CT LAgentSpeak(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. ProcMsg
ClrInt1 AchvGl ClrInt3
ClrInt TestGl1 TestGl2
AddBel DelBel SelEv1 ClrInt2
SelEv2 SelInt2 Action
SelInt
SelInt1 ExecInt
Appl2 Appl1 ExtEv IntEv
SelAppl SelAppl
AddIM SelEv
RelPl
Rel1
ApplPl – 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 LAgentSpeak(L) may be seen as an instance of BDICT L. Similar approaches
have been accomplished for other programming languages [
To specify the temporal behavior we use CT L∗ in the next way.
formula s: – s ::= φ|s ∧ s|¬s – p ::= s|¬p|p ∧ p|Ep|Ap|
p|♦p| p|p U p 4.4
Semantics of BDIACST(LL)
Initially the semantics of BEL, DES and INT is adopted from [
fined in terms of an agent ag and its configuration ag, C, M, T, s :
BEL ag,C,M,T,s (φ) ≡ φ ∈ bs INT ag,C,M,T,s (φ) ≡ φ ∈ agoals(i) ∨
agoals(i) i∈CI
te,i ∈CE
DES ag,C,M,T,s (φ) ≡ +!φ, i ∈ CE ∨ INT(φ) where CI denotes current intentions and CE suspended intentions. By now we have a defeasible framework for intentions that lacks temporal representation; 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 intention φ in N BDIACST(LL) 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 φ[gc], 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. – S is a set of agent configurations c = ag, C, M, T, s . – Γ ⊆ S2 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. ∀γ[gc] ∈ I, γ[gc] fails at ∆ or 2.2.2.2. ψ[g ] γ[gc] 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(∀φ[gc] ∈ I : ¬BEL(ctx(φ)) ∨ ∃ψ[g ] ∈ body(φ) ∼| ψ[g ]) or 4.2.2.1. ∃γ[gc] ∈ I s.t. γ[gc] succeds at ∆ and 4.2.2.2. ψ[g ] γ[gc] 4.6
Now we suggest a square of opposition in order to describe some desired properties of the system.
φ 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.
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.
φ.
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.
φ < < ∨ s ∨ < |∼ φ < k c r > ∼| φ > ∨ s > ∨ > φ Corollary 3 (Coherence) If is false that |∼ φ.
φ then it is false that φ. And if If ∼| φ then it
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
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 configurations σ 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Γβ = agent in a model.
SΓβ , RΓβ , V denotes a run of an
Γ 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 Definition 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 |= φ.
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Γβ |= ¬φ; > φ
∨ > =| φ 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
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 [
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 reviewers for their useful comments and precise corrections. The first author is supported by the CONACyT scholarship 214783.