Sequent systems for compact bilinear logic

Mathematical Logic Quarterly 49 (5):467 (2003)
  Copy   BIBTEX

Abstract

Compact Bilinear Logic , introduced by Lambek [14], arises from the multiplicative fragment of Noncommutative Linear Logic of Abrusci [1] by identifying times with par and 0 with 1. In this paper, we present two sequent systems for CBL and prove the cut-elimination theorem for them. We also discuss a connection between cut-elimination for CBL and the Switching Lemma from [14].

Categories

Keywords

Reprint years

DOI

10.1002/malq.200310050

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,928

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Sequent Calculi for Visser's Propositional Logics.Kentaro Kikuchi & Ryo Kashima - 2001 - Notre Dame Journal of Formal Logic 42 (1):1-22.
Synchronized Linear-Time Temporal Logic.Heinrich Wansing & Norihiro Kamide - 2011 - Studia Logica 99 (1-3):365-388.
Varieties of linear calculi.Sara Negri - 2002 - Journal of Philosophical Logic 31 (6):569-590.
A normalizing system of natural deduction for intuitionistic linear logic.Sara Negri - 2002 - Archive for Mathematical Logic 41 (8):789-810.
A proof-theoretic treatment of λ-reduction with cut-elimination: λ-calculus as a logic programming language.Michael Gabbay - 2011 - Journal of Symbolic Logic 76 (2):673 - 699.
Logic and Grammar.Joachim Lambek - 2012 - Studia Logica 100 (4):667-681.
Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic.V. Michele Abrusci - 1991 - Journal of Symbolic Logic 56 (4):1403-1451.
The Geometry of Non-Distributive Logics.Greg Restall & Francesco Paoli - 2005 - Journal of Symbolic Logic 70 (4):1108 - 1126.
The deduction rule and linear and near-linear proof simulations.Maria Luisa Bonet & Samuel R. Buss - 1993 - Journal of Symbolic Logic 58 (2):688-709.
Temporal non-commutative logic: Expressing time, resource, order and hierarchy.Norihiro Kamide - 2009 - Logic and Logical Philosophy 18 (2):97-126.
Deep sequent systems for modal logic.Kai Brünnler - 2009 - Archive for Mathematical Logic 48 (6):551-577.
An approach to infinitary temporal proof theory.Stefano Baratella & Andrea Masini - 2004 - Archive for Mathematical Logic 43 (8):965-990.
Algebraic aspects of cut elimination.Francesco Belardinelli, Peter Jipsen & Hiroakira Ono - 2004 - Studia Logica 77 (2):209 - 240.
SN and {CR} for free-style {${bf LK}sp {tq}$}: linear decorations and simulation of normalization.Jean-Baptiste Joinet, Harold Schellinx & Lorenzo Tortora de Falco - 2002 - Journal of Symbolic Logic 67 (1):162-196.

Analytics

Added to PP
2013-12-01

Downloads
15 (#947,515)

6 months
7 (#430,392)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

On the logic of β -pregroups.Aleksandra Kiślak-Malinowska - 2007 - Studia Logica 87 (2-3):323 - 342.
On the Logic of β-pregroups.Aleksandra Kiślak-Malinowska - 2007 - Studia Logica 87 (2-3):323-342.

View all 7 citations / Add more citations

References found in this work

Completeness Results for Lambek Syntactic Calculus.Wojciech Buszkowski - 1986 - Mathematical Logic Quarterly 32 (1‐5):13-28.
Completeness Results for Lambek Syntactic Calculus.Wojciech Buszkowski - 1986 - Mathematical Logic Quarterly 32 (1-5):13-28.
The finite model property for various fragments of linear logic.Yves Lafont - 1997 - Journal of Symbolic Logic 62 (4):1202-1208.
A tale of four grammars.Claudia Casadio & Joachim Lambek - 2002 - Studia Logica 71 (3):315-329.

Add more references