  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 not 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, a
new programming language called 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, 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.
