Abstract: Intention production is the procedure that BDI Agent drafts an action sequence to realize a goal. However, it is also a big obstacle to verify the validity of Agent intention produced by the specification of Agent Programming Languagc(API).In this paper, to prove the validity of intention execution in AgentSpeak, we constructed a model-theoretic semantics and a formal interpretation of Agent programs intention. Then, on the bases of the model-theoretic semantics and the operational semantics presented by Moreira and I3ordini, we proved the equivalence theorem; the intention in model-theoretic semantics of AgentSpcak language is equivalent with the one in operational semantics of AgentSpeak program According to the ectuivalence theorem, we can get the conclusion that intention execution of AgentSpeak is sound and complete.

Key words: AgentSpeak, Intention production, Agent programming language, Model-theoretic semantics, BDI Agent