Clausal resolution in a logic of rational agency

Dixon, Clare, Fisher, Michael and Bolotov, Alexander (2002) Clausal resolution in a logic of rational agency. Artificial Intelligence: an international journal, 139 (1). pp. 47-89. ISSN 0004-3702

Full text not available from this repository.
Official URL:


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.

Item Type: Article
Uncontrolled Keywords: Verification, Rational agents, Automated deduction, Resolution, Temporal logics, Modal logics
Subjects: University of Westminster > Science and Technology > Electronics and Computer Science, School of (No longer in use)
Depositing User: Users 4 not found.
Date Deposited: 22 Sep 2005
Last Modified: 14 Oct 2009 09:25

Actions (login required)

Edit Item (Repository staff only) Edit Item (Repository staff only)