document: Clausal resolution in a logic of rational agency 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 -LRB- representing change over time -RRB- with the modal logic KD45 -LRB- representing belief -RRB- . 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
doc_bio_tags: O O O O O O O O O B I I I O O B I O O B O O O O O O O O O O O B I B O O O O O O O O B I B O O B O O O O O O O B I O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O
extractive_keyphrases: resolution based proof system temporal logic ctl modal logic kd45 belief dynamic logics
abstractive_keyphrases: branching-time temporal logic multi-agent systems multi-modal logics rational agents