A verification framework for agent programming with declarative goals

F. S. de Boer, K. V. Hindriks, W. van der Hoek*, J. J.Ch Meyer

*Corresponding author for this work

Research output: Contribution to JournalArticleAcademicpeer-review


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.

Original languageEnglish
Pages (from-to)277-302
Number of pages26
JournalJournal of Applied Logic
Issue number2
Publication statusPublished - 1 Jun 2007
Externally publishedYes


  • Agent programming language
  • Agents
  • Beliefs
  • Declarative goals
  • Programming logic


Dive into the research topics of 'A verification framework for agent programming with declarative goals'. Together they form a unique fingerprint.

Cite this