A clausal resolution method for branching-time logic ECTL+

We expand the applicability of the clausal resolution technique to the branching-time temporal logic ECTL_. ECTL_ is strictly more expressive than the basic computation tree logic CTL and its extension, ECTL, as it allows Boolean combinations of fairness and single temporal operators. We show that any ECTL_ formula can be translated to a normal form the structure of which was initially defined for CTL and then applied to ECTL. This enables us to apply to ECTL_ a resolution technique defined over the set of clauses. Our correctness argument also bridges the gap in the correctness proof for ECTL: we show that the transformation procedure for ECTL preserves unsatisfiability