WestminsterResearch

Clausal resolution in a logic of rational agency

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

Abstract

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
Research Community:University of Westminster > Electronics and Computer Science, School of
ID Code:487
Deposited On:22 Sep 2005
Last Modified:14 Oct 2009 10:25

Repository Staff Only: item control page