Towards an algorithmic construction of cut-elimination procedures

DOI10.1017/S0960129507006573MaRDI QIDQ5458060zbMATH OpenFDO

Authors Agata Ciabattoni, Alexander Leitsch

Publication date 10 April 2008

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/S0960129507006573

zbMATH Keywords

resolutionsequent calculisubstructural logicscut eliminationknotted structural rules

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Cut-elimination and normal-form theorems (03F05) Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1138593
• Cut elimination theorems and a canonical model construction for some implicational substructural logics
• Structural cut elimination. I: Intuitionistic and classical logic
• Cut Elimination and Decidability for Classical Lambek Logic
• Cut-elimination and redundancy-elimination by resolution

Cites work

• scientific article; zbMATH DE number 976360 (Why is no real title available?)
• Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL
• Automated complexity analysis based on ordered resolution
• Bounded contraction and Gentzen-style formulation of Łukasiewicz logics
• Cut-elimination and redundancy-elimination by resolution
• Extending intuitionistic linear logic with knotted structural rules
• Implication of clauses is undecidable
• Non-deterministic Multiple-valued Structures
• On the Specification of Sequent Systems
• Towards a semantic characterization of cut-elimination
• Untersuchungen über das logische Schliessen. I

Cited in

(20)

• The way we were: structural operational semantics research in perspective
• Cut Elimination and Decidability for Classical Lambek Logic
• Computer Science Logic
• Which structural rules admit cut elimination? An algebraic criterion
• Extension without cut
• Cut-Elimination for SBL
• Cut elimination for GLS using the terminability of its regress process
• Book review of: Matthias Baaz and Alexander Leitsch, Methods of cut-elimination
• Cut and pay
• Algebraic aspects of cut elimination
• Multi-focused cut elimination
• Cut-elimination and proof schemata
• Towards Algorithmic Cut-Introduction
• Cut-elimination for \(\omega_{1}\)
• Cut elimination for shallow modal logics
• Towards a semantic characterization of cut-elimination
• Sufficient conditions for cut elimination with complexity analysis
• Sharpened lower bounds for cut elimination
• Cut-admissibility as a corollary of the subformula property
• Cut-elimination and redundancy-elimination by resolution

This page was built for publication: Towards an algorithmic construction of cut-elimination procedures

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