Constructing refinement operators by decomposing logical implication