Towards an algorithmic construction of cut-elimination procedures

DOI10.1017/S0960129507006573zbMath1138.03043MaRDI QIDQ5458060

Agata Ciabattoni, Alexander Leitsch

Publication date: 10 April 2008

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

zbMATH Keywords

cut eliminationresolutionsubstructural logicssequent calculiknotted structural rules

Mathematics Subject Classification ID

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

Related Items (3)

Cut-Elimination and Proof Schemata ⋮ Cut Elimination for Shallow Modal Logics ⋮ Extension without cut

Cites Work

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

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