Structures for Multiplicative Cyclic Linear Logic: Deepness vs Cyclicity

The aim of this work is to give an alternative presentation for the multiplicative fragment of Yetter’s cyclic linear logic. The new presentation is inspired by the calculus of structures, and has the interesting feature of avoiding the cyclic rule. The main point in this work is to show how cyclicity can be substituted by deepness, i.e. the possibility of applying an inference rule at any point of a formula. We finally derive, through a new proof technique, the cut elimination property of the calculus.

• Type: Conference
• Year: 2004
• Where: CSL
• Authors: Pietro Di Gianantonio
• Keywords: CSL 2004, Cyclic Rule, Multiplicative Fragment, Yetter’s Cyclic Linear