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.