Building Decision Procedures for Modal Logics from Propositional Decision Procedures - The Case Study of Modal K