Algorithmic proof methods and cut elimination for implicational logics part I: Modal implication

Studia Logica 61 (2):237-280 (1998)
  Copy   BIBTEX


In this work we develop goal-directed deduction methods for the implicational fragment of several modal logics. We give sound and complete procedures for strict implication of K, T, K4, S4, K5, K45, KB, KTB, S5, G and for some intuitionistic variants. In order to achieve a uniform and concise presentation, we first develop our methods in the framework of Labelled Deductive Systems [Gabbay 96]. The proof systems we present are strongly analytical and satisfy a basic property of cut admissibility. We then show that for most of the systems under consideration the labelling mechanism can be avoided by choosing an appropriate way of structuring theories. One peculiar feature of our proof systems is the use of restart rules which allow to re-ask the original goal of a deduction. In case of K, K4, S4 and G, we can eliminate such a rule, without loosing completeness. In all the other cases, by dropping such a rule, we get an intuitionistic variant of each system. The present results are part of a larger project of a goal directed proof theory for non-classical logics; the purpose of this project is to show that most implicational logics stem from slight variations of a unique deduction method, and from different ways of structuring theories. Moreover, the proof systems we present follow the logic programming style of deduction and seem promising for proof search [Gabbay and Reyle 84, Miller et al. 91].



    Upload a copy of this work     Papers currently archived: 91,088

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

Goal-directed proof theory.Dov M. Gabbay - 2000 - Boston: Kluwer Academic. Edited by Nicola Olivetti.
Deduction theorems for weak implicational logics.M. W. Bunder - 1982 - Studia Logica 41 (2-3):95 - 108.
Labelled non-classical logics.Luca Viganò - 2000 - Boston: Kluwer Academic Publishers.
Proof theory of modal logic.Heinrich Wansing (ed.) - 1996 - Boston: Kluwer Academic Publishers.
Uniqueness of normal proofs in implicational intuitionistic logic.Takahito Aoto - 1999 - Journal of Logic, Language and Information 8 (2):217-242.
Implicational f-structures and implicational relevance logics.A. Avron - 2000 - Journal of Symbolic Logic 65 (2):788-802.


Added to PP

44 (#327,510)

6 months
6 (#252,172)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Dov Gabbay
Hebrew University of Jerusalem