Agent logics as program logics: Grounding KARO

Koen V. Hindriks*, John Jules Ch Meyer

*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review


Several options are available to relate agent logics to computational agent systems. Among others, one can try to find useful executable fragments of an agent logic or use a model checking approach. In this paper, an alternative approach is explored based on the view that an agent logic is a program logic. Using the same starting point, one of the established agent logics, we ask instead if it is possible to construct a programming language for that agent logic. We show that the programming language and the agent logic are formally related by constructing a denotational semantics. As a result, the agent logic can be used as as a design tool to specify and verify the corresponding agent programs. In particular, we construct an agent programming language that is formally related to the KARO agent logic. The KARO logic is an agent logic that builds on top of dynamic logic. The approach is based on mapping worlds in the modal semantics for KARO onto a state-based semantics. The state-based semantics can be used to define an operational semantics for KARO programs. In this way, we obtain a computationally grounded semantics for a significant part of the KARO logic, including the operators for knowledge or beliefs, motivational attitudes and belief revision actions of a rational KARO agent.

Original languageEnglish
Title of host publicationKI 2006
Subtitle of host publicationAdvances in Artificial Intelligence - 29th Annual German Conference on AI, KI 2006, Proceedings
Number of pages15
Volume4314 LNAI
Publication statusPublished - 29 Oct 2007
Externally publishedYes
Event29th Annual German Conference on Artificial Intelligence (KI 2006) - Bremen, Germany
Duration: 14 Jun 200617 Jun 2006


Conference29th Annual German Conference on Artificial Intelligence (KI 2006)


Dive into the research topics of 'Agent logics as program logics: Grounding KARO'. Together they form a unique fingerprint.

Cite this