Contraction-free sequent calculi for intuitionistic logic
From MaRDI portal
Publication:4032862
DOI10.2307/2275431zbMath0761.03004MaRDI QIDQ4032862
Publication date: 1 April 1993
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2307/2275431
03F05: Cut-elimination and normal-form theorems
03B20: Subsystems of classical logic (including intuitionistic logic)
Related Items
A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs, European Summer Meeting of the Association for Symbolic Logic, Proof-theoretical investigation of temporal logic with time gaps, Subtractive logic, Graph-based decision for Gödel-Dummett logics, The ILTP problem library for intuitionistic logic, Inconsistency-tolerant description logic. II: A tableau algorithm for \(\mathcal{CALC}^{\mathsf C}\), Optimization techniques for propositional intuitionistic logic and their implementation, Interpolation in non-classical logics, Focusing and polarization in linear, intuitionistic, and classical logics, Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi, Linearizing intuitionistic implication, Representing scope in intuitionistic deductions, Permutability of proofs in intuitionistic sequent calculi, An improved refutation system for intuitionistic predicate logic, A linear logical framework, Correspondences between classical, intuitionistic and uniform provability, Connection methods in linear logic and proof nets construction, Proof-search in type-theoretic languages: An introduction, Infinitary calculus for a restricted first-order linear temporal logic without contraction on quantified formulas, Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem, Sufficient conditions for cut elimination with complexity analysis, Decision methods for linearly ordered Heyting algebras, Eigenvariables, bracketing and the decidability of positive minimal predicate logic, Invertible infinitary calculus without loop rules for restricted FTL, Labelled Calculi for Łukasiewicz Logics, Deep Inference in Bi-intuitionistic Logic, Intuitionistic Socratic procedures, A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications, Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme, 1998 European Summer Meeting of the Association for Symbolic Logic
Cites Work
- Computational interpretations of linear logic
- Proof methods for modal and intuitionistic logics
- Logics without the contraction rule
- Efficient loop detection in prolog using the tortoise-and-hare technique
- A Note on Gentzen's Decision Procedure for Intuitionistic Propositional Logic
- Proving termination with multiset orderings
- On an interpretation of second order quantification in first order intuitionistic propositional logic
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
