Search Strategies for Resolution in CTL-Type Logics: Extension and Complexity

A clausal resolution approach originally developed for the branching logic CTL has recently been extended to the logics ECTL and ECTL+ . In the application of the resolution rules searching for a loop is essential. In this paper we define a Depth-First technique to complement the existing Breadth-First Search and provide the complexity analysis of the developed methods. Additionally, it contains a correction in our previous presentation of loops.

• Type: Conference
• Year: 2005
• Where: TIME
• Authors: Artie Basukoski, Alexander Bolotov
• Keywords: Branching Logic Ctl, Clausal Resolution Approach, Logical Reasoning, Resolution Rules, TIME 2005