Encoding Modal Logics in Logical Frameworks