Clausal resolution in a logic of rational agency

Citations of this article
Mendeley users who have this article in their library.


A resolution based proof system for a Temporal Logic of Possible Belief is presented. This logic is the combination of the branching-time temporal logic CTL (representing change over time) with the modal logic KD45 (representing belief). Such combinations of temporal or dynamic logics and modal logics are useful for specifying complex properties of multi-agent systems. Proof methods are important for developing verification techniques for these complex multi-modal logics. Soundness, completeness and termination of the proof method are shown and simple examples illustrating its use are given. © 2002 Elsevier Science B.V. All rights reserved.




Dixon, C., Fisher, M., & Bolotov, A. (2002). Clausal resolution in a logic of rational agency. Artificial Intelligence, 139(1), 47–89.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free