1999/10/31 by Alessio Guglielmi · 2 citations
Computer Science · #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.LO
paper · pdf · doi:10.1145/1182613.1182614
published as ACM Transactions on Computational Logic, Vol. 8 (1:1), 2007, pp. 1-64 · 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>
openalex publication_date 2007/01/01 · arxiv created 2007/01/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.