Soundness and Completeness Proof of Agent Intention Production in AgentSpeak
AgentSpeak中意图生成过程的可靠性与完整性研究

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.