Research

A system of interaction and structure


Reference:

Guglielmi, A., 2007. A system of interaction and structure. ACM Transactions on Computational Logic, 8 (1).

Related documents:

This repository does not currently have the full-text of this item.
You may be able to access a copy if URLs are provided below.

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.

Details

Item Type Articles
CreatorsGuglielmi, A.
DOI10.1145/1182613.1182614
DepartmentsFaculty of Science > Computer Science
RefereedYes
StatusPublished
ID Code5286
Additional InformationID number: ISI:000244402200001

Export

Actions (login required)

View Item