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

DOI10.1007/978-3-031-39784-4_24MaRDI QIDQ6199592zbMATH OpenFDO

Authors Niccolò Veltri

Publication date 28 February 2024

Published in Logic, Language, Information, and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-031-39784-4_24

zbMATH Keywords

Agdamaximal multi-focusingskew monoidal closed categoriesskew non-commutative MILLsubstructural logics

Mathematics Subject Classification ID

Logic in computer science (03B70)

Cites work

• A multi-focused proof system isomorphic to expansion proofs
• A sequent calculus for a semi-associative law
• Coherence via focusing for symmetric skew monoidal categories
• Focusing and polarization in linear, intuitionistic, and classical logics
• Linear logic
• Logic Programming with Focusing Proofs in Linear Logic
• Monads need not be endofunctors
• Multi-focused cut elimination
• Multi-focused proofs with different polarity assignments
• Multi-focusing on extensional rewriting with sums
• Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic
• Skew-closed categories
• The sequent calculus of skew monoidal categories
• Which simple types have a unique inhabitant?

Cited in

(4)

• Coherence via focusing for symmetric skew monoidal and symmetric skew closed categories
• Semi-substructural logics à la Lambek
• Semi-substructural logics with additives
• Semi-substructural logics à la Lambek with symmetry

This page was built for publication: Maximally multi-focused proofs for skew non-commutative \texttt{MILL}

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