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

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

• 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