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

Studia Logica 61 (2):237-280 (1998)
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].
Keywords Philosophy   Logic   Mathematical Logic and Foundations   Computational Linguistics
Categories (categorize this paper)
Reprint years 2004
DOI 10.1023/A:1005077431494
 Save to my reading list
Follow the author(s)
Edit this record
My bibliography
Export citation
Find it on Scholar
Mark as duplicate
Request removal from index
Revision history
Download options
Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 29,530
Through your library
References found in this work BETA

No references found.

Add more references

Citations of this work BETA
Dual-Context Sequent Calculus and Strict Implication.Kentaro Kikuchi - 2002 - Mathematical Logic Quarterly 48 (1):87-92.

Add more citations

Similar books and articles
Added to PP index

Total downloads
20 ( #266,127 of 2,210,873 )

Recent downloads (6 months)
2 ( #208,006 of 2,210,873 )

How can I increase my downloads?

Monthly downloads
My notes
Sign in to use this feature