ECAI-2000 Logo

ECAI-2000 Conference Paper

[PDF] [full paper] [prev] [tofc] [next]

Resolution in a Logic of Rational Agency

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.


[prev] [tofc] [next]


ECAI-2000 is organised by the European Coordinating Committee for Artificial Intelligence (ECCAI) and hosted by the Humboldt University on behalf of Gesellschaft für Informatik.