Multi-focused cut elimination

DOI10.1017/S0960129516000451zbMath1456.03093MaRDI QIDQ4637625

Taus Brock-Nannestad, Nicolas Guenot

Publication date: 25 April 2018

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

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Related Items

Maximally multi-focused proofs for skew non-commutative \texttt{MILL}

Cites Work

• Linear logic
• A framework for proof systems
• A logical characterization of forward and backward chaining in the inverse method
• Focusing and polarization in linear, intuitionistic, and classical logics
• Proof nets, garbage, and computations
• Untersuchungen über das logische Schliessen. I
• Polarized proof-nets and \(\lambda \mu\)-calculus
• Structural Focalization
• From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
• Logic Programming with Focusing Proofs in Linear Logic
• Focused Natural Deduction
• Focusing Strategies in the Sequent Calculus of Synthetic Connectives
• Least and Greatest Fixed Points in Linear Logic
• Focused linear logic and the \(\lambda\)-calculus
• Unnamed Item
• Unnamed Item
• Unnamed Item