Clare Dixon, Michael Fisher, Alexander Bolotov
A resolution based proof system for a Temporal Logic of Possible Belief is presented and justified. This logic represents a combination of the branching-time temporal logic CTL and the modal logic KD45. Since such combinations of non-classical logics are often used in agent theories for specifying complex properties of rational agents, the resolution system presented here provides a basis for the verification of such specifications.
Keywords: Automated Reasoning, Temporal Reasoning, Multi-Agent Systems, Theorem Proving, Deduction
Citation: Clare Dixon, Michael Fisher, Alexander Bolotov: Resolution in a Logic of Rational Agency. In W.Horn (ed.): ECAI2000, Proceedings of the 14th European Conference on Artificial Intelligence, IOS Press, Amsterdam, 2000, pp.358-362.