Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic

DOI10.2307/2275485MaRDI QIDQ3984416zbMATH OpenOpenAlexFDO

Authors V. Michele Abrusci

Publication date 27 June 1992

Published in Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2307/2275485

zbMATH Keywords

completenesscut eliminationcut rulenoncommutative linear logicnoncommutative monoid with unitone-sided sequent calculiphase spacesplanar graphsproof-netspropositional logicsemanticssoundnesstwo-sided sequent calculus

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07)

Recommendations

• Phase semantics for a pure noncommutative linear propositional logic
• Non-commutative logic II: sequent calculus and phase semantics
• Non-commutative logic. I: The multiplicative fragment

Cites work

• Constructing locales from quantales
• Linear logic
• Non‐commutative intuitionistic linear logic

Cited in

(66)

• Natural deduction and coherence for weakly distributive categories
• Phase semantics for a pure noncommutative linear propositional logic
• A generalization of analytic deduction via labelled deductive systems. I: Basic substructural logics
• Handsome proof-nets: Perfect matchings and cographs
• A graph-theoretic characterization theorem for multiplicative fragment of non-commutative linear logic
• Proof-search in type-theoretic languages: An introduction
• Some lattice models of bilinear logic
• Relations and non-commutative linear logic
• Linear Läuchli semantics
• Non-commutative logic. I: The multiplicative fragment
• On phase semantics and denotational semantics in multiplicative-additive linear logic
• Proof diagrams for multiplicative linear logic: syntax and semantics
• Contrary-to-duty reasoning: a categorical approach
• A geometrical representation of the basic laws of categorial grammar
• On involutive nonassociative Lambek calculus
• Proper semantics for substructural logics, from a stalker theoretic point of view
• Type logics and pregroups
• Parsing pregroup grammars and Lambek calculus using partial composition
• Lambek calculus is NP-complete
• Proof-search and proof nets in mixed linear logic
• Exchange rules
• Finite models of some substructural logics
• Multiplicative linear logics and fibrations
• Strong negation in intuitionistic style sequent systems for residuated lattices
• On classical nonassociative Lambek calculus
• Orthogonality and Boolean Algebras for Deduction Modulo
• A system of interaction and structure. V: The exponentials and splitting
• 2005 Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '05
• Graphs of plural cuts
• The shuffle Hopf algebra and noncommutative full completeness
• Representation Theorems for Quantales
• Autonomous posets and quantales
• The finite model property for various fragments of linear logic
• Non-commutative logic II: sequent calculus and phase semantics
• Involutive nonassociative Lambek calculus: sequent systems and complexity
• Categorial grammars and their logics
• Non-commutative classical arithmetical sequent calculi are intuitionistic
• scientific article; zbMATH DE number 218517 (Why is no real title available?)
• scientific article; zbMATH DE number 1841813 (Why is no real title available?)
• Classical linear logics with mix separation principle
• European Summer Meeting of the Association for Symbolic Logic
• Hopf algebras and linear logic
• Residuated frames with applications to decidability
• Galois connections in categorial type logic
• One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity
• Pomset logic. The other approach to noncommutativity in logic
• scientific article; zbMATH DE number 7441265 (Why is no real title available?)
• Linear exponential comonads without symmetry
• A phase semantics for polarized linear logic and second order conservativity
• Coherence for Frobenius pseudomonoids and the geometry of linear proofs
• On canonical embeddings of residuated groupoids
• Word order alternation in Sanskrit via precyclicity in pregroup grammars
• Holomorphic models of exponential types in linear logic
• Relational Models for the Lambek Calculus with Intersection and Constants
• A computational algebraic analysis of Hindi syntax
• Explorations in Subexponential Non-associative Non-commutative Linear Logic
• Cut elimination and strong separation for substructural logics: an algebraic approach
• Weakly distributive categories
• A semantic proof of generalised cut elimination for deep inference
• Sequent systems for consequence relations of cyclic linear logics
• An algebraic investigation of linear logic
• YALLA: yet another deep embedding of linear logic in Rocq
• Extending computational trinitarianism
• A computational algebraic approach to Latin grammar
• Symmetric categorial grammar
• Multi-adjoint algebras versus non-commutative residuated structures

This page was built for publication: Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic

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