TY - JOUR
T1 - A verification framework for agent programming with declarative goals
AU - de Boer, F. S.
AU - Hindriks, K. V.
AU - van der Hoek, W.
AU - Meyer, J. J.Ch
PY - 2007/6/1
Y1 - 2007/6/1
N2 - A long and lasting problem in agent research has been to close the gap between agent logics and agent programming frameworks. The main reason for this problem of establishing a link between agent logics and agent programming frameworks is identified and explained by the fact that agent programming frameworks have hardly incorporated the concept of a declarative goal. Instead, such frameworks have focused mainly on plans or goals-to-do instead of the end goals to be realised which are also called goals-to-be. In this paper, the programming language GOAL is introduced which incorporates such declarative goals. The notion of a commitment strategy-one of the main theoretical insights due to agent logics, which explains the relation between beliefs and goals-is used to construct a computational semantics for GOAL. Finally, a proof theory for proving properties of GOAL agents is introduced. Thus, the main contribution of this paper, rather than the language GOAL itself, is that we offer a complete theory of agent programming in the sense that our theory provides both for a programming framework and a programming logic for such agents. An example program is proven correct by using this programming logic.
AB - A long and lasting problem in agent research has been to close the gap between agent logics and agent programming frameworks. The main reason for this problem of establishing a link between agent logics and agent programming frameworks is identified and explained by the fact that agent programming frameworks have hardly incorporated the concept of a declarative goal. Instead, such frameworks have focused mainly on plans or goals-to-do instead of the end goals to be realised which are also called goals-to-be. In this paper, the programming language GOAL is introduced which incorporates such declarative goals. The notion of a commitment strategy-one of the main theoretical insights due to agent logics, which explains the relation between beliefs and goals-is used to construct a computational semantics for GOAL. Finally, a proof theory for proving properties of GOAL agents is introduced. Thus, the main contribution of this paper, rather than the language GOAL itself, is that we offer a complete theory of agent programming in the sense that our theory provides both for a programming framework and a programming logic for such agents. An example program is proven correct by using this programming logic.
KW - Agent programming language
KW - Agents
KW - Beliefs
KW - Declarative goals
KW - Programming logic
UR - http://www.scopus.com/inward/record.url?scp=34247154931&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=34247154931&partnerID=8YFLogxK
U2 - 10.1016/j.jal.2005.12.014
DO - 10.1016/j.jal.2005.12.014
M3 - Article
AN - SCOPUS:34247154931
SN - 1570-8683
VL - 5
SP - 277
EP - 302
JO - Journal of Applied Logic
JF - Journal of Applied Logic
IS - 2
ER -