A system of interaction and structure
Top Cited Papers
- 1 January 2007
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Computational Logic
- Vol. 8 (1), 1
- https://doi.org/10.1145/1182613.1182614
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.Keywords
Other Versions
This publication has 18 references indexed in Scilit:
- A System of Interaction and Structure II: The Need for Deep InferenceLogical Methods in Computer Science, 2006
- System NEL is UndecidableElectronic Notes in Theoretical Computer Science, 2003
- Two Restrictions on ContractionLogic Journal of the IGPL, 2003
- Non-commutative logic II: sequent calculus and phase semanticsMathematical Structures in Computer Science, 2000
- Relating Natural Deduction and Sequent Calculus for Intuitionistic Non-Commutative Linear LogicElectronic Notes in Theoretical Computer Science, 1999
- Non-commutative logic I: the multiplicative fragmentAnnals of Pure and Applied Logic, 1999
- Forum: A multiple-conclusion specification logicTheoretical Computer Science, 1996
- Games and full completeness for multiplicative linear logicThe Journal of Symbolic Logic, 1994
- Logic Programming with Focusing Proofs in Linear LogicJournal of Logic and Computation, 1992
- Linear logicTheoretical Computer Science, 1987