Modal resolution in standard clausal form

The modal resolution system given by P. Enjalbert and L. Farinas del Cerro (1989) has two disadvantages. One is the symbol redundancy in their system, the other is that there are many resolvent computing rules and these rules are defined recursively. In this paper, we give a notion of a standard clause set for a modal clause set. A method called standard resolution is presented, which is based on the standard clause set for propositional modal logic. We prove that any set of modal clauses is unsatisfiable if and only if there is a standard resolution deduction of an empty clause from its standard clause set. Thus, the soundness and completeness for standard resolution is proved. The new method is intuitive, has only one resolution rule and can easily be achieved due to its simple inference rule. The result of an experiment shows that our method is more efficient than the one of P. Enjalbert and L. Farinas del Cerro