Contraction-free sequent calculi for intuitionistic logic

DOI10.2307/2275431zbMATH Open0761.03004OpenAlexW2131739376MaRDI QIDQ4032862FDOQ4032862

Authors: Roy Dyckhoff 

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

Recommendations

• CONTRACTION-FREE SEQUENT CALCULI FOR INTUITIONISTIC LOGIC: A CORRECTION
• Admissibility of structural rules for contraction-free systems of intuitionistic logic
• On permuting cut with contraction
• Contraction-elimination for implicational logics
• On a contraction-less intuitionistic propositional logic with conjunction and fusion

zbMATH Keywords

contraction ruleintuitionistic propositional calculusmodifications of natural deduction

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)

Cites Work

• Title not available (Why is that?)
• Proving termination with multiset orderings
• Computational interpretations of linear logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Proof methods for modal and intuitionistic logics
• Logics without the contraction rule
• On an interpretation of second order quantification in first order intuitionistic propositional logic
• Title not available (Why is that?)
• Efficient loop detection in prolog using the tortoise-and-hare technique
• A Note on Gentzen's Decision Procedure for Intuitionistic Propositional Logic

Cited In (84)

• Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem
• CONTRACTION-FREE SEQUENT CALCULI FOR INTUITIONISTIC LOGIC: A CORRECTION
• A timing refinement of intuitionistic proofs and its application to the timing analysis of combinational circuits
• The G4i analogue of a G3i sequent calculus
• Optimization techniques for propositional intuitionistic logic and their implementation
• Analyticity, balance and non-admissibility of \textit{Cut} in stoic logic
• An evaluation-driven decision procedure for G3i
• A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications
• Eigenvariables, bracketing and the decidability of positive minimal predicate logic
• Interpolation in non-classical logics
• Contraction contracted
• An improved refutation system for intuitionistic predicate logic
• Synthesis of modality definitions and a theorem prover for epistemic intuitionistic logic
• Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
• Inconsistency-tolerant description logic. II: A tableau algorithm for \(\mathcal{CALC}^{\mathsf C}\)
• Subtractive logic
• Linearizing intuitionistic implication
• Labelled Calculi for Łukasiewicz Logics
• From cut-free calculi to automated deduction: the case of bounded contraction
• Representing scope in intuitionistic deductions
• \(\mathsf{ileanTAP}\): an intuitionistic theorem prover
• Decision methods for linearly ordered Heyting algebras
• European Summer Meeting of the Association for Symbolic Logic
• Sequent Calculi for Intuitionistic Linear Logic with Strong Negation
• A Cut-Free and Invariant-Free Sequent Calculus for PLTL
• Terminating calculi and countermodels for constructive modal logics
• Uniform interpolation and the existence of sequent calculi
• The ILTP problem library for intuitionistic logic
• Loop-check specification for a sequent calculus of temporal logic
• Intuitionistic Decision Procedures Since Gentzen
• Correspondences between classical, intuitionistic and uniform provability
• Composition of an intuitionistic negation and negative modalities as a necessity operator
• Note on deduction theorems in contraction-free logics
• Admissibility of structural rules for contraction-free systems of intuitionistic logic
• Permutability of proofs in intuitionistic sequent calculi
• Two loop detection mechanisms: a comparison
• A linear logical framework
• The Tableau Workbench
• A resolution theorem prover for intuitionistic logic
• Generalized tableau systems for intermediate propositional logics
• Efficient loop-check for backward proof search in some non-classical propositional logics
• A sequent calculus for a negative free logic
• Proofs and countermodels in non-classical logics
• Intuitionistic Socratic procedures
• Sequent calculi for intuitionistic Gödel-Löb logic
• Proof Search and Counter Model of Positive Minimal Predicate Logic
• Intuitionistic propositional logic without `contraction' but with `reductio'
• Efficient SAT-based proof search in intuitionistic propositional logic
• SAT-based proof search in intermediate propositional logics
• Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
• On implicational intermediate logics axiomatizable by formulas minimal in classical logic: a counter-example to the Komori-Kashima problem
• Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models
• Focusing and polarization in linear, intuitionistic, and classical logics
• Practical Proof Search for Coq by Type Inhabitation
• Sufficient conditions for cut elimination with complexity analysis
• Graph-based decision for Gödel-Dummett logics
• Refined typing to localize the impact of forced strictness on free theorems
• Title not available (Why is that?)
• Contraction-free proofs and finitary games for linear logic
• Geometrisation of first-order logic
• Hammer for Coq: automation for dependent type theory
• Connection methods in linear logic and proof nets construction
• Proof-search in type-theoretic languages: An introduction
• Proof-search in intuitionistic logic based on constraint satisfaction
• \textsc{Minlog}: a minimal logic theorem prover
• Infinitary calculus for a restricted first-order linear temporal logic without contraction on quantified formulas
• Contraction-elimination for implicational logics
• Eigenvariables, bracketing and the decidability of positive minimal intuitionistic logic
• Invertible infinitary calculus without loop rules for restricted FTL
• Deciding intuitionistic propositional logic via translation into classical logic
• 1998 European Summer Meeting of the Association for Symbolic Logic
• An intuitionistic formula hierarchy based on high‐school identities
• Interactive matching logic proofs in Coq
• General clauses for SAT-based proof search in intuitionistic propositional logic
• Proof theory for Lax Logic
• An ecumenical notion of entailment
• A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs
• Title not available (Why is that?)
• Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi
• Deep Inference in Bi-intuitionistic Logic
• Proof-theoretical investigation of temporal logic with time gaps
• A unified procedure for provability and counter-model generation in minimal implicational logic
• Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis
• On Dummett's pragmatist justification procedure

This page was built for publication: Contraction-free sequent calculi for intuitionistic logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4032862)