A system of interaction and structure

Research output: Contribution to journalArticle

82 Citations (Scopus)

Abstract

This article introduces a logical system, called BV, which extends multiplicative linear logic by a noncommutative self-dual logical operator. This extension is particularly challenging for the sequent calculus, and so far, it is not achieved therein. It becomes very natural in a new formalism, called the calculus of structures, which is the main contribution of this work. Structures are formulas subject to certain equational laws typical of sequents. The calculus of structures is obtained by generalizing the sequent calculus in such a way that a new top-down symmetry of derivations is observed, and it employs inference rules that rewrite inside structures at any depth. These properties, in addition to allowing the design of BV, yield a modular proof of cut elimination.
Original languageEnglish
JournalACM Transactions on Computational Logic
Volume8
Issue number1
DOIs
Publication statusPublished - 2007

Fingerprint

Sequent Calculus
Interaction
Calculus
Logical operator
Cut-elimination
Linear Logic
Inference Rules
Multiplicative
Symmetry
Design

Cite this

A system of interaction and structure. / Guglielmi, A.

In: ACM Transactions on Computational Logic, Vol. 8, No. 1, 2007.

Research output: Contribution to journalArticle

@article{3d037fc917f74645a24c160a5272dca6,
title = "A system of interaction and structure",
abstract = "This article introduces a logical system, called BV, which extends multiplicative linear logic by a noncommutative self-dual logical operator. This extension is particularly challenging for the sequent calculus, and so far, it is not achieved therein. It becomes very natural in a new formalism, called the calculus of structures, which is the main contribution of this work. Structures are formulas subject to certain equational laws typical of sequents. The calculus of structures is obtained by generalizing the sequent calculus in such a way that a new top-down symmetry of derivations is observed, and it employs inference rules that rewrite inside structures at any depth. These properties, in addition to allowing the design of BV, yield a modular proof of cut elimination.",
author = "A Guglielmi",
note = "ID number: ISI:000244402200001",
year = "2007",
doi = "10.1145/1182613.1182614",
language = "English",
volume = "8",
journal = "ACM Transactions on Computational Logic",
issn = "1529-3785",
publisher = "Association for Computing Machinery",
number = "1",

}

TY - JOUR

T1 - A system of interaction and structure

AU - Guglielmi, A

N1 - ID number: ISI:000244402200001

PY - 2007

Y1 - 2007

N2 - This article introduces a logical system, called BV, which extends multiplicative linear logic by a noncommutative self-dual logical operator. This extension is particularly challenging for the sequent calculus, and so far, it is not achieved therein. It becomes very natural in a new formalism, called the calculus of structures, which is the main contribution of this work. Structures are formulas subject to certain equational laws typical of sequents. The calculus of structures is obtained by generalizing the sequent calculus in such a way that a new top-down symmetry of derivations is observed, and it employs inference rules that rewrite inside structures at any depth. These properties, in addition to allowing the design of BV, yield a modular proof of cut elimination.

AB - This article introduces a logical system, called BV, which extends multiplicative linear logic by a noncommutative self-dual logical operator. This extension is particularly challenging for the sequent calculus, and so far, it is not achieved therein. It becomes very natural in a new formalism, called the calculus of structures, which is the main contribution of this work. Structures are formulas subject to certain equational laws typical of sequents. The calculus of structures is obtained by generalizing the sequent calculus in such a way that a new top-down symmetry of derivations is observed, and it employs inference rules that rewrite inside structures at any depth. These properties, in addition to allowing the design of BV, yield a modular proof of cut elimination.

U2 - 10.1145/1182613.1182614

DO - 10.1145/1182613.1182614

M3 - Article

VL - 8

JO - ACM Transactions on Computational Logic

JF - ACM Transactions on Computational Logic

SN - 1529-3785

IS - 1

ER -