Resolution in a logic of rational agency
Clare Dixon, Michael Fisher, Alexander Bolotov · European Conference on Artificial Intelligence · 2000
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.