Abstract. We present the design of 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 SLDresolution calculi for modal logics, including calculi for useful multimodal logics of belief. It is a tool to experiment with applications of modal logic programming to AI.