To overcome the notation redundancy in the modaI resolution systems estab-lished bv P．Enjalbert and L．Farinas del Cerro，the authors propose marked modal resolu-tion．whose soundness and completeness are proved．In marked modal resolution，they mark possible operators in modal clauses，and add a rule for computing resolvent of two formulas which are bound by possible operator respectively．This new method has the fol-lowing feature：a resolvent may not be a logical consequence of its parents，it is only a log-ical consequence of the input set of clauses,that iS the soundness．At the same time，they design and implement system RD based on modal resolution of Enjalbert and Farinas del Cerro．and system MRD based on marked modal resolution in C-PROLOG，and then run on SUN workstation．The experimental results show：the MRD method iS almostly 10 times faster than RD．