We introduce our implemented modal logic programming system MProlog. This system is written in Prolog as a module for Prolog. Codes, libraries, and most features of Prolog can be used in MProlog programs. The system contains a number of built-in SLD-resolution calculi for modal logics, including calculi for useful multimodal logics of belief. Modal logics can be used to reason about knowledge, belief, actions, etc. A number of authors have proposed modal extensions for logic programming; see [7] for a survey and [6, 1, 3, 4] for later works. There are two approaches for modal logic programming: the direct approach and the translational approach. The first approach directly uses modalities, while the second one translates modal logic programs to classical logic programs. Despite that the theory of modal logic programming has been studied in a considerable number of works, it has not received much attention in practice. But if we want to use modal logics for practical applications, then...