A System of Interaction and Structure

Abstract

This paper introduces a logical system, called BV, which extends multiplicative linear logic by a non-commutative 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 formulae submitted to certain equational laws typical of sequents. The calculus of structures is obtained by generalising 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 allow the design of BV, yield a modular proof of cut elimination.

This is the authoritative version of the article, with readable pictures, in colour, also available at <http://cs.bath.ac.uk/ag/p/SystIntStr.pdf>. (The published version contains errors introduced by the editorial processing.) Web site for Deep Inference and the Calculus of Structures at <http://alessio.guglielmi.name/res/cos>

References in corpus (1)

• A System of Interaction and Structure II: The Need for Deep Inference

Cited by in corpus (44)

• A System of Interaction and Structure II: The Need for Deep Inference
• Normalisation Control in Deep Inference via Atomic Flows
• Cirquent calculus deepened
• On the Proof Complexity of Deep Inference
• The three dimensions of proofs
• A System of Interaction and Structure IV: The Exponentials and Decomposition
• When You Must Forget: beyond strong persistence when forgetting in answer set programming
• Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae
• The taming of recurrences in computability logic through cirquent calculus, Part I
• Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Procedures
• Extending a system in the calculus of structures with a self-dual quantifier
• Subatomic Proof Systems: Splittable Systems
• A Provenance Tracking Model for Data Updates
• De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic
• On Structuring Proof Search for First Order Linear Logic
• On noncommutative extensions of linear logic
• An Analytic Propositional Proof System on Graphs
• Interaction and Depth against Nondeterminism in Proof Search
• A System of Interaction and Structure III: The Complexity of BV and Pomset Logic
• Constrained path-finding and structure from acyclicity
• Beyond formulas-as-cographs: an extension of Boolean logic to arbitrary graphs
• Pomset logic: the other approach to non commutativity in logic
• Prioritise the Best Variation
• On the Pre- and Promonoidal Structure of Spacetime
• Formulas as Processes, Deadlock-Freedom as Choreographies (Extended Version)
• Linear lambda Calculus with Explicit Substitutions as Proof-Search in Deep Inference
• An Intuitionistic Formula Hierarchy Based on High-School Identities
• Towards a Denotational Semantics for Proofs in Constructive Modal Logic
• Communication, and concurrency with logic-based restriction inside a calculus of structures
• Consistency Without Cut Elimination
• Inducing syntactic cut-elimination for indexed nested sequents
• Clausal Resolution for Modal Logics of Confluence
• Canonical Abstract Syntax Trees
• A Subatomic Proof System for Decision Trees
• A Deep Inference System for Differential Linear Logic
• A Sequent Calculus for Modelling Interferences
• Subatomic systems need not be subatomic
• Locality for Classical Logic
• Composing Dinatural Transformations: Towards a Calculus of Substitution
• Internal and External Calculi: Ordering the Jungle without Being Lost in Translations
• A Semantic Proof of Generalised Cut Elimination for Deep Inference
• Exponentially Handsome Proof Nets and Their Normalization
• Flag: a Self-Dual Modality for Non-Commutative Contraction and Duplication in the Category of Coherence Spaces
• Enumerating Independent Linear Inferences