Towards a semantic characterization of cut-elimination

DOI10.1007/s11225-006-6607-2zbMath1105.03057OpenAlexW2166144087MaRDI QIDQ817704

Kazushige Terui, Agata Ciabattoni

Publication date: 17 March 2006

Published in: Studia Logica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11225-006-6607-2

zbMATH Keywords

sequent calculussubstructural logicsphase semanticscut-eliminationnonclassical logics

Mathematics Subject Classification ID

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

Related Items

Hypersequent rules with restricted contexts for propositional modal logics, Cut elimination in coalgebraic logics, Algebraic proof theory for substructural logics: cut-elimination and completions, Sufficient conditions for cut elimination with complexity analysis, Orthogonality and Boolean Algebras for Deduction Modulo, Kripke Semantics for Basic Sequent Systems, Basic Constructive Connectives, Determinism and Matrix-Based Semantics, New consecution calculi for \(R^{t}_{\to}\), Strict Canonical Constructive Systems, Algebraic proof theory: hypersequents and hypercompletions, Towards an algorithmic construction of cut-elimination procedures, Canonical Calculi: Invertibility, Axiom Expansion and (Non)-determinism, Finite-valued semantics for canonical labelled calculi

Cites Work

• Extending intuitionistic linear logic with knotted structural rules
• Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic
• A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
• Algebraic aspects of cut elimination
• Display logic
• Untersuchungen über das logische Schliessen. I
• Bounded contraction and Gentzen-style formulation of Łukasiewicz logics
• Non‐commutative intuitionistic linear logic
• Computer Science Logic
• Which structural rules admit cut elimination? An algebraic criterion
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item