Contraction-free sequent calculi for intuitionistic logic

DOI10.2307/2275431zbMath0761.03004OpenAlexW2131739376MaRDI QIDQ4032862

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

zbMATH Keywords

intuitionistic propositional calculuscontraction rulemodifications of natural deduction

Mathematics Subject Classification ID

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

Related Items (69)

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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

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