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

DOI10.2307/2275485zbMath0746.03044OpenAlexW2074070481MaRDI QIDQ3984416

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

completeness cut elimination propositional logic planar graphs semantics cut rule soundness phase spaces proof-nets noncommutative linear logic noncommutative monoid with unit one-sided sequent calculi two-sided sequent calculus

Mathematics Subject Classification ID

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

Related Items (51)

The shuffle Hopf algebra and noncommutative full completeness ⋮ A geometrical representation of the basic laws of categorial grammar ⋮ Holomorphic models of exponential types in linear logic ⋮ Unnamed Item ⋮ A generalization of analytic deduction via labelled deductive systems. I: Basic substructural logics ⋮ European Summer Meeting of the Association for Symbolic Logic ⋮ Symmetric categorial grammar ⋮ Some lattice models of bilinear logic ⋮ Strong negation in intuitionistic style sequent systems for residuated lattices ⋮ Relations and non-commutative linear logic ⋮ Unnamed Item ⋮ Linear Läuchli semantics ⋮ Representation Theorems for Quantales ⋮ Autonomous posets and quantales ⋮ Natural deduction and coherence for weakly distributive categories ⋮ Graphs of plural cuts ⋮ Linear Exponential Comonads without Symmetry ⋮ Handsome proof-nets: Perfect matchings and cographs ⋮ A graph-theoretic characterization theorem for multiplicative fragment of non-commutative linear logic ⋮ On involutive nonassociative Lambek calculus ⋮ Proper semantics for substructural logics, from a stalker theoretic point of view ⋮ Multi-adjoint algebras versus non-commutative residuated structures ⋮ Relational Models for the Lambek Calculus with Intersection and Constants ⋮ On Classical Nonassociative Lambek Calculus ⋮ A computational algebraic analysis of Hindi syntax ⋮ Cut elimination and strong separation for substructural logics: an algebraic approach ⋮ Involutive Nonassociative Lambek Calculus: Sequent Systems and Complexity ⋮ Unnamed Item ⋮ Categorial Grammars and Their Logics ⋮ Hopf algebras and linear logic ⋮ Finite Models of Some Substructural Logics ⋮ Orthogonality and Boolean Algebras for Deduction Modulo ⋮ Weakly distributive categories ⋮ Type logics and pregroups ⋮ Parsing pregroup grammars and Lambek calculus using partial composition ⋮ Exchange rules ⋮ The finite model property for various fragments of linear logic ⋮ Residuated frames with applications to decidability ⋮ On Canonical Embeddings of Residuated Groupoids ⋮ Word Order Alternation in Sanskrit via Precyclicity in Pregroup Grammars ⋮ Galois Connections in Categorial Type Logic ⋮ A phase semantics for polarized linear logic and second order conservativity ⋮ Lambek calculus is NP-complete ⋮ Phase semantics for a pure noncommutative linear propositional logic ⋮ Proof-search in type-theoretic languages: An introduction ⋮ Multiplicative Linear Logics and Fibrations ⋮ One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity ⋮ Proof diagrams for multiplicative linear logic: syntax and semantics ⋮ 2005 Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '05 ⋮ Contrary-to-duty reasoning: a categorical approach ⋮ A computational algebraic approach to Latin grammar

Cites Work

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