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)|
References found in this work BETA
No references found.
Citations of this work BETA
Dual-Context Sequent Calculus and Strict Implication.Kentaro Kikuchi - 2002 - Mathematical Logic Quarterly 48 (1):87-92.
Similar books and articles
Fibred Semantics and the Weaving of Logics Part 1: Modal and Intuitionistic Logics.D. M. Gabbay - 1996 - Journal of Symbolic Logic 61 (4):1057-1120.
Deduction Theorems for Weak Implicational Logics.M. W. Bunder - 1982 - Studia Logica 41 (2-3):95 - 108.
Substructural Implicational Logics Including the Relevant Logic E.Ryo Kashima & Norihiro Kamide - 1999 - Studia Logica 63 (2):181-212.
On Modal Logics Characterized by Models with Relative Accessibility Relations: Part II.Stéphane Demri & Dov Gabbay - 2000 - Studia Logica 66 (3):349-384.
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 index2009-01-28
Total downloads18 ( #258,237 of 2,032,467 )
Recent downloads (6 months)1 ( #397,033 of 2,032,467 )
How can I increase my downloads?
There are no threads in this forum
Nothing in this forum yet.