Contraction-free sequent calculi for intuitionistic logic

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

Cites work

scientific article; zbMATH DE number 42059 (Why is no real title available?)
scientific article; zbMATH DE number 46359 (Why is no real title available?)
scientific article; zbMATH DE number 49746 (Why is no real title available?)
scientific article; zbMATH DE number 192927 (Why is no real title available?)
scientific article; zbMATH DE number 3557754 (Why is no real title available?)
A Note on Gentzen's Decision Procedure for Intuitionistic Propositional Logic
Computational interpretations of linear logic
Efficient loop detection in prolog using the tortoise-and-hare technique
Logics without the contraction rule
On an interpretation of second order quantification in first order intuitionistic propositional logic
Proof methods for modal and intuitionistic logics
Proving termination with multiset orderings

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
Optimization techniques for propositional intuitionistic logic and their implementation
The G4i analogue of a G3i sequent calculus
A timing refinement of intuitionistic proofs and its application to the timing analysis of combinational circuits
Analyticity, balance and non-admissibility of \textit{Cut} in stoic logic
Eigenvariables, bracketing and the decidability of positive minimal intuitionistic logic
Invertible infinitary calculus without loop rules for restricted FTL
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
Deciding intuitionistic propositional logic via translation into classical logic
Interpolation in non-classical logics
An improved refutation system for intuitionistic predicate logic
Contraction contracted
1998 European Summer Meeting of the Association for Symbolic Logic
Synthesis of modality definitions and a theorem prover for epistemic intuitionistic logic
Inconsistency-tolerant description logic. II: A tableau algorithm for \(\mathcal{CALC}^{\mathsf C}\)
Linearizing intuitionistic implication
Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
An intuitionistic formula hierarchy based on high‐school identities
Subtractive logic
From cut-free calculi to automated deduction: the case of bounded contraction
Labelled Calculi for Łukasiewicz Logics
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
Terminating calculi and countermodels for constructive modal logics
Interactive matching logic proofs in Coq
A Cut-Free and Invariant-Free Sequent Calculus for PLTL
Sequent Calculi for Intuitionistic Linear Logic with Strong Negation
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
General clauses for SAT-based proof search in intuitionistic propositional 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
A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs
An ecumenical notion of entailment
Proof theory for Lax Logic
Note on deduction theorems in contraction-free logics
Permutability of proofs in intuitionistic sequent calculi
Admissibility of structural rules for contraction-free systems of intuitionistic logic
A linear logical framework
Two loop detection mechanisms: a comparison
scientific article; zbMATH DE number 7455712 (Why is no real title available?)
The Tableau Workbench
A resolution theorem prover for intuitionistic logic
Generalized tableau systems for intermediate propositional logics
A sequent calculus for a negative free logic
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi
Efficient loop-check for backward proof search in some non-classical propositional logics
Deep Inference in Bi-intuitionistic Logic
Proofs and countermodels in non-classical logics
Sequent calculi for intuitionistic Gödel-Löb logic
Intuitionistic Socratic procedures
Intuitionistic propositional logic without `contraction' but with `reductio'
Proof Search and Counter Model of Positive Minimal Predicate Logic
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
A unified procedure for provability and counter-model generation in minimal implicational logic
Proof-theoretical investigation of temporal logic with time gaps
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
Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis
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
On Dummett's pragmatist justification procedure
Graph-based decision for Gödel-Dummett logics
Refined typing to localize the impact of forced strictness on free theorems
Contraction-free proofs and finitary games for linear logic
scientific article; zbMATH DE number 823590 (Why is no real title available?)
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
Infinitary calculus for a restricted first-order linear temporal logic without contraction on quantified formulas
Contraction-elimination for implicational logics
\textsc{Minlog}: a minimal logic theorem prover

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)