Proof diagrams for multiplicative linear logic: syntax and semantics

DOI10.1007/S10817-018-9466-4MaRDI QIDQ2331072zbMATH OpenOpenAlexFDO

Authors Matteo Acclavio

Publication date 25 October 2019

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1702.00268

zbMATH Keywords

linear logicmonoidal categoriesproof semanticsstring diagrams

Mathematics Subject Classification ID

Structure of proofs (03F07) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Monoidal categories, symmetric monoidal categories (18M05)

Abstract: Proof nets are a syntax for linear logic proofs which gives a coarser notion of proof equivalence with respect to syntactic equality together with an intuitive geometrical representation of proofs. In this paper we give an alternative $2$-dimensional syntax for multiplicative linear logic derivations. The syntax of string diagrams authorizes the definition of a framework where the sequentializability of a term, i.e. deciding whether the term corresponds to a correct derivation, can be verified in linear time. Furthermore, we can use this syntax to define a denotational semantics for multiplicative linear logic with units by means of equivalence classes of proof diagrams modulo a terminating rewriting.

Recommendations

• Proof diagrams for multiplicative linear logic
• scientific article; zbMATH DE number 937366
• Computer Science Logic
• Proof nets sequentialisation in multiplicative linear logic
• Coherent models of proof nets

Cites work

• A new constructive logic: classic logic
• A prehistory of \(n\)-categorical physics
• A survey of graphical languages for monoidal categories
• Categorical semantics of linear logic
• Computer Science Logic
• Higher-dimensional categories with finite derivation type
• Higher-dimensional word problems with applications to equational logic
• scientific article; zbMATH DE number 786485 (Why is no real title available?)
• scientific article; zbMATH DE number 786495 (Why is no real title available?)
• scientific article; zbMATH DE number 937366 (Why is no real title available?)
• scientific article; zbMATH DE number 3367095 (Why is no real title available?)
• INTRODUCTION TO THE YANG-BAXTER EQUATION
• Limits indexed by category-valued 2-functors
• Linear logic
• No proof nets for MLL with units: proof equivalence in MLL is PSPACE-complete
• Parsing MELL proof nets
• Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic
• Proof diagrams for multiplicative linear logic
• Termination orders for three-dimensional rewriting
• The geometry of tensor calculus. I
• The structure of multiplicatives
• Towards an algebraic theory of Boolean circuits.

Cited in

(12)

• Proof theory for heterogeneous logic combining formulas and diagrams: proof normalization
• Implicit exchange in multiplicative proofnets
• Proof nets as formal Feynman diagrams
• From proof-nets to bordisms: the geometric meaning of multiplicative connectives
• Retractile Proof Nets of the Purely Multiplicative and Additive Fragment of Linear Logic
• Proof diagrams for multiplicative linear logic
• scientific article; zbMATH DE number 7441265 (Why is no real title available?)
• A categorical reduction system for linear logic
• Computer Science Logic
• scientific article; zbMATH DE number 2208067 (Why is no real title available?)
• Canonicity of proofs in constructive modal logic
• Exponentially handsome proof nets and their normalization

This page was built for publication: Proof diagrams for multiplicative linear logic: syntax and semantics

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