Building decision procedures for modal logics from propositional decision procedures: the case study of modal K(m)