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

cut eliminationknotted structural rulesresolutionsequent calculisubstructural logics

Mathematics Subject Classification ID

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

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

• 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
• scientific article; zbMATH DE number 976360 (Why is no real title available?)
• 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

(21)

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

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)