On correspondence between modal and classical logic: automated approach

Szalas, Andrzej

アイテム詳細

登録内容を編集ファイル形式で保存

一時保存へ追加

タグ情報を表示リリース履歴を表示詳細要約

公開

報告書

On correspondence between modal and classical logic: automated approach

MPS-Authors

Szalas, Andrzej
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

There are no locators available

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

フルテキスト (公開)

MPI-I-92-209.pdf
(全文テキスト（全般）), 119KB

付随資料 (公開)

There is no public supplementary material available

引用

Szalas, A.(1992). On correspondence between modal and classical logic: automated approach (MPI-I-92-209). Saarbrücken: Max-Planck-Institut für Informatik.

引用: https://hdl.handle.net/11858/00-001M-0000-0014-B1BE-5

要旨

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.