@INPROCEEDINGS{Hustadt+Dixon+Schmidt+Fisher+Meyer+van_der_Hoek@TIME2001,
 AUTHOR        = {Hustadt, Ullrich and Dixon, Clare and Schmidt, Renate A. and 
 Fisher, Michael and Meyer, John-Jules and van der Hoek, Wiebe},
 TITLE         = {Reasoning about agents in the {KARO} framework},
 BOOKTITLE     = {Proceedings of the Eighth International Symposium on Temporal Representation and Reasoning 
 (TIME-01) [Cividale del Friuli, Italy, 14-16 June 2001]},
 YEAR          = {2001},
 EDITOR        = {Bettini, Claudio and Montanari, Angelo},
 PAGES         = {206-213},
 PUBLISHER     = {IEEE Press},
 PADDRESS      = {Los Alamitos, CA, USA},
 PYEAR         = {2001},
 CADDRESS      = {Cividale del Friuli, Italy},
 CYEAR         = {2001},
 CMONTH        = jun # {~14--16},
 URL           = {Hustadt+Dixon+Schmidt+Fisher+Meyer+van_der_Hoek@TIME2001.pdf},
 URL           = {http://doi.ieeecomputersociety.org/10.1109/TIME.2001.930719},
 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.}
}