On an Automated Translation of Modal Proof Rules into Formulas of the Classical Logic
Article in journal (Refereed)
Journal of Applied Non-Classical Logics(ISSN 1166-3081)
Engineering and Technology
automated theorem proving, correspondence theory, modal logics
In this paper we study correspondences between modal proof rules and the classical logic. The method we apply is based on an Ackermann's technique of eliminating second-order quantifiers from formulas. We show that the process of finding suitable correspondences can be reduced to a few simple steps. Moreover, the whole technique can be fully mechanized. We thus provide the reader with a powerful tool, useful in automated translations between modal logics and the classical logic.