In this paper we give an algorithm of automatic theorem proving for various modal predicate systems, and prove its completeness. These modal systems can be tanslated into two-sorted extensional system. Using this fact, the theorem proving can be implemented by using the resolution for the extensional systems. Especially our new results in this paper are two inference rules for S4-modal system, which give a shorter proof than the ordinary resolution.

In this paper we have represented a model structure of modal lower (first-order) predicate logic (S5) (abbr. MLPC in our paper) in two-sorted extensional language (abbr. EL2), and tried to translate a formula of MLPC into a formula of two-sorted logic (abbr. ELPC) in such a way as preserving provability. (i.e.P in MLPC iff P* in ELPC, where P* is the translation of P). Roughly speaking, modal symbol (necessity) is translated into the universal quantifier k of the domain which expresses the set of possible worlds, and n-ary predicates are n1 -ary predicates. For instance, xP (x) is translated into kx*P* (x*, k), where * denotes the translation. Therefore it is possible to replace a theorem proving of MLPC with that of two-sorted logic ELPC, so we have shown it possible to prove a theorem of MLPC by using the resolution principle in ELPC. Then the completeness of the resolution in two-sorted logic is proved, and a normal form of MLPC is introduced. It is shown that for any formula of MLPC there exists an algorithm to transform the formula into its normal form. This normal form is obtained by decreasing the number of modal symbol in a formula as possible. For instance, xP (x) yQ (y) is transformed into xy (P (x) Q (y)).