The Soundness and Completeness Proof of Agent Intention in AgentSpeak

Autonomy is one of the characteristics that agent has which distinguish agent systems from the other conceptualisations within Computer Science. To prove the validity of intention execution in AgentSpeak, according to the agent´s goal, we construct a model-theoretic semantics of AgentSpeak and an informal interpretation of agent program. Then we give an equivalence theorem of intention execution for AgentSpeak that the sequence of actions produced by an agent written in AgentSpeak is equivalent with the intention produced by the model that satisfies the belief set and plan set of agent.