Search

Global property is the necessary condition which must be satisfied by the provable formulus. It can help us to find out some unprovable formula that doesn't satisfy some global property before we start proving it by any formal automated reasoning system, thus the efficiency of the whole system is improved. We present some global property of valid formulus in modal logic K. Such a property is a structure character of the formula, so it is simple and easy to check.

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.