U. Hustadt, C. Dixon, R. A. Schmidt, M. Fisher, J.-J. Meyer, and W. van der Hoek (2001): ``Reasoning about agents in the KARO framework.'' In C. Bettini and A. Montanari, editors, Proceedings of the Eighth International Symposium on Temporal Representation and Reasoning TIME-01 [Cividale del Friuli, Italy, 14-16 June 2001], pp. 206-213. IEEE Press.
Abstract, BibTeX, PDF (© IEEE Press).

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 $\ml{CTL}$ and multi-modal $\ml{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. [an error occurred while processing this directive]