Dixon, Clare and 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: http://dx.doi.org/10.1016/S0004-3702(02)00196-0
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.
|Uncontrolled Keywords:||Verification, Rational agents, Automated deduction, Resolution, Temporal logics, Modal logics|
|Research Community:||University of Westminster > Electronics and Computer Science, School of|
|Deposited On:||22 Sep 2005|
|Last Modified:||14 Oct 2009 10:25|
Repository Staff Only: item control page