Reasoning about Agents in the KARO Framework

Hustadt, U., Dixon, C., Schmidt, R. A., Fisher, M., Meyer, J.-J. and van der Hoek, W. (2001)

In Bettini, C. and Montanari, A. (eds), Proceedings of the Eighth International Symposium on Temporal Representation and Reasoing (TIME'2001). IEEE Computer Society, 206-213. BiBTeX.

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.


Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 01 Mar 04
Copyright © 2001 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk