Skip navigation
Skip navigation

A system of interaction and structure II: the need for deep inference

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...[Show more]

CollectionsANU Research Publications
Date published: 2006-04-03
Type: Journal article
Source: Logical Methods in Computer Science
DOI: 10.2168/LMCS-2(2:4)2006


File Description SizeFormat Image
Tiu_System2006.pdf635.56 kBAdobe PDFThumbnail

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator