## Tiu, Alwen - 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
A System of Interaction and Structure II: The Need for Deep Inference

Authors: Tiu, Alwen

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.

Source : oai:arXiv.org:cs/0512036
DOI : 10.2168/LMCS-2(2:4)2006
Volume: Volume 2, Issue 2
Published on: April 3, 2006
Submitted on: November 21, 2016
Keywords: Computer Science - Logic in Computer Science,F.4.1