On the Relational Translation Method for Propositional Modal Logics

TL;DR

This paper demonstrates the practical effectiveness of the relational translation method for propositional modal logics by using first-order theorem provers and model generators to prove theorems and show invalidities.

Contribution

It shows that the relational translation approach is feasible in practice and compares different methods for reasoning in propositional modal logics.

Findings

Successfully proved many benchmark modal theorems using first-order theorem provers.

Identified small models for many satisfiable formulas.

Compared various approaches for modal logic reasoning.

Abstract

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.