@INPROCEEDINGS{HustadtDixonEtal01a,
AUTHOR = {Hustadt, U. and Dixon, C. and Schmidt, R. A. and Fisher, M. and Meyer, J.-J. and van der Hoek, W.},
YEAR = {2001},
TITLE = {Reasoning about Agents in the {KARO} Framework},
EDITOR = {Bettini, C. and Montanari, A.},
BOOKTITLE = {Proceedings of the Eighth International Symposium on Temporal Representation and Reasoing (TIME'2001)},
PUBLISHER = {IEEE Computer Society},
ADDRESS = {Los Alamitos, California},
PAGES = {206--213},
URL = {http://www.cs.man.ac.uk/~schmidt/publications/HustadtDixonEtal01a.html},
ISBN = {0-7695-1107-4},
ISSN = {1530-1311},
ABSTRACT = {
This paper proposes two methods for realising automated reasoning
about agent-based systems. The framework for modelling intelligent
agent behaviour that we focus on is a core of KARO logic, an expressive
combination of various modal logics including propositional dynamic
logic, a modal logic of knowledge, a modal logic of wishes, and
additional non-standard operators.
The first method we present is based on a translation of core KARO
logic to first-order logic combined with first-order resolution. The
second method uses an embedding of core KARO logic into a combination
of branching-time temporal logic CTL and multi-modal S5
plus a clausal resolution calculus for these 
combined logics. We discuss the advantages and shortcomings of each
approach and suggest ways to extend each variant to cover more of the
KARO framework.  
}
}