On the Relational Translation Method for Propositional Modal Logics

One way of proving theorems in modal logics is translating them into the predicate calculus and then using conventional resolution-style theorem provers. This approach has been regarded as inappropriate in practice, because the resulting formulas are too lengthy and it is impossible to show the non-theoremhood of modal formulas. In this paper, we demonstrate the practical feasibility of the (relational) translation method. Using a state-of-the-art theorem prover for first-order predicate logic, we proved many benchmark theorems available from the modal logic literature. We show the invalidity of propositional modal and temporal logic formulas, using model generators or satisfiability testers for the classical logic. Many satisfiable formulas are found to have very small models. Finally, several different approaches are compared.