LiU Electronic Press
Full-text not available in DiVA
Author:
Szalas, Andrzej (University of Warsaw)
Title:
On the Correspondence between Modal and Classical Logic: An Automated Approach
Publication type:
Article in journal (Refereed)
Language:
English
Publisher: Oxford University Press
Status:
Published
In:
Journal of logic and computation (Print)(ISSN 0955-792X)(EISSN 1465-363X)
Volume:
3
Issue:
6
Pages:
605-620
Year of publ.:
1993
URI:
urn:nbn:se:liu:diva-74977
Permanent link:
http://urn.kb.se/resolve?urn=urn:nbn:se:liu:diva-74977
Subject category:
Engineering and Technology
Keywords(en) :
Automated theorem proving, correspondence axioms, modal logics, semantics-based translation
Abstract(en) :

The current paper is devoted to automated techniques in the correspondence theory. The theory we deal with concerns the problem of finding classical first-order axioms corresponding to propositional modal schemas. Given a modal schema and a semantics base  method of translating propositional modal formulae into classical first-order ones, we try to derive automatically classica first-order formulae characterizing precisely the class of frames validating the schema. The technique we consider can, in many cases, be easily applied even without computer support. Although we mainly concentrate on Kripke semantics, the technique we apply is much more general, as it is based on elimination of second-order quantifiers from formulae. We show many examples of application of the method. These can also serve as new, automated proofs of considered correspondences.                 

Available from:
2012-02-13
Created:
2012-02-13
Last updated:
2012-02-22
Statistics:
11 hits