On an Automated Translation of Modal Proof Rules into Formulas of the Classical Logic
1994 (English)In: Journal of Applied Non-Classical Logics, ISSN 1166-3081, Vol. 4, no 2, 119-127Article in journal (Refereed) Published
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.
automated theorem proving, correspondence theory, modal logics
National CategoryEngineering and Technology
IdentifiersURN: urn:nbn:se:liu:diva-74979OAI: oai:DiVA.org:liu-74979DiVA: diva2:499789