A Polynomial Translation Of S4 Into T And Contraction–free Tableaux For S4

Logic Journal of the IGPL 5 (2):287-300 (1997)
  Copy   BIBTEX

Abstract

The concern of this paper is the study of automated deduction methods for propositional modal logics. We use tableau proof-systems to show that Fitting's translation of the transitive modal logic S4 into T can be constructed in deterministic polynomial time. This result is exploited in order to establish a polynomial bound to the length of branches in both tableau and sequent proof search for the transitive logics S4 and K4. This allows the elimination of “periodicity tests” when proving S4-validity; moreover, it provides directly a form of “contraction elimination result” in modal sequent calculi, in the sense that the number of contractions needed in a branch of a sequent proof need not exceed a given polynomial function of the endsequent. In order to obtain a complete contraction free fragment of the sequent calculus for S4, Mints' translation of modal formulae into modal clauses is used. Mints' notion of modal clause is also used to provide polynomial translations of S4 and K4 into K, by means of a preliminary rewriting of the input formulae into clausal form

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 98,418

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

A contraction-free sequent calculus for S4.Jörg Hudelmaier - 1996 - In Heinrich Wansing (ed.), Proof theory of modal logic. Boston: Kluwer Academic Publishers. pp. 3--15.
Herbrand style proof procedures for modal logic.Marta Cialdea - 1993 - Journal of Applied Non-Classical Logics 3 (2):205-223.
Modal translations in substructural logics.Kosta Došen - 1992 - Journal of Philosophical Logic 21 (3):283 - 336.
Cut Elimination for Extended Sequent Calculi.Simone Martini, Andrea Masini & Margherita Zorzi - 2023 - Bulletin of the Section of Logic 52 (4):459-495.
Labeled sequent calculi for modal logics and implicit contractions.Pierluigi Minari - 2013 - Archive for Mathematical Logic 52 (7-8):881-907.
Transfer of sequent calculus strategies to resolution for S4.Grigori Mints, Vladimir Orevkov & Tanel Tammet - 1996 - In Heinrich Wansing (ed.), Proof theory of modal logic. Boston: Kluwer Academic Publishers. pp. 2--17.
Stable Modal Logics.Guram Bezhanishvili, Nick Bezhanishvili & Julia Ilin - 2018 - Review of Symbolic Logic 11 (3):436-469.

Analytics

Added to PP
2015-02-04

Downloads
8 (#1,536,914)

6 months
5 (#929,326)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references