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.