Alwen Tiu - A System of Interaction and Structure II: The Need for Deep Inference

lmcs:2252 - Logical Methods in Computer Science, April 3, 2006, Volume 2, Issue 2 - https://doi.org/10.2168/LMCS-2(2:4)2006
A System of Interaction and Structure II: The Need for Deep InferenceArticle

Authors: Alwen Tiu

    This paper studies properties of the logic BV, which is an extension of multiplicative linear logic (MLL) with a self-dual non-commutative operator. BV is presented in the calculus of structures, a proof theoretic formalism that supports deep inference, in which inference rules can be applied anywhere inside logical expressions. The use of deep inference results in a simple logical system for MLL extended with the self-dual non-commutative operator, which has been to date not known to be expressible in sequent calculus. In this paper, deep inference is shown to be crucial for the logic BV, that is, any restriction on the ``depth'' of the inference rules of BV would result in a strictly less expressive logical system.


    Volume: Volume 2, Issue 2
    Published on: April 3, 2006
    Submitted on: July 5, 2005
    Keywords: Computer Science - Logic in Computer Science,F.4.1

    14 Documents citing this article

    Consultation statistics

    This page has been seen 992 times.
    This article's PDF has been downloaded 379 times.