A TRANSLATION APPROACH TO MODAL LOGIC REASONING

A translation approach to modal logic reasoning is studied.This method tries to prove a modal theorem by translating it into a formula in the classic logic, and then proves the formula by using a conventional theorem prover. It is pointed out that the translation approach preserves the decidability of propositional normal modal logics.Some experimental results are also given,which show that the method is practical.