Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


On correspondence between modal and classical logic: automated approach

Szalas, Andrzej

MPI-I-92-209. March 1992, 17 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
The current paper is devoted to automated techniques in 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 based method of translating propositional modal formulas into classical first-order ones, we try to derive automatically classical first-order formula characterizing precisely the class of frames validating the schema. The technique we consider can, in many cases, be easily applied even without any 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 formulas. We show many examples of application of the method. Those can also serve as new, automated proofs of considered correspondences.

We essentially strengthen the considered elimination technique. Thus, as a side-effect of this paper we get a stronger elimination based method for proving a subset of second-order logic.
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-92-209.pdfMPI-I-92-209.pdfMPI-I-92-209.dvi70 KBytes; 119 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document:
Hide details for BibTeXBibTeX
  AUTHOR = {Szalas, Andrzej},
  TITLE = {On correspondence between modal and classical logic: automated approach},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-92-209},
  MONTH = {March},
  YEAR = {1992},
  ISSN = {0946-011X},