We show how to decide modal logics by the inverse method. Unlike the semantics-based tableau method, the inverse method only derives tautologies, so search space pruning using semantics is difficult, if possible at all. We demonstrate how one can find redundancy criteria for sequents and derivations using syntactic properties of derivations in sequent calculi.