We show that every connected Multiplicative Exponential Linear Logic (MELL) proof-structure (with or without cuts) is uniquely determined by a well-chosen element of its Taylor expansion: the one obtained by taking two copies of the content of each box. As a consequence, the relational model is injective with respect to connected MELL proof-structures.
|Titolo:||Computing connected proof(-structure)s from their Taylor expansion|
|Data di pubblicazione:||2016|
|Citazione:||Giulio, G., Luc, P., & TORTORA DE FALCO, L. (2016). Computing connected proof(-structure)s from their Taylor expansion. In proceedings of the conference ``Formal Structures for Computation and Deduction'', Porto (Portugal), 22-25 june 2016.|
|Appare nelle tipologie:||4.1 Contributo in Atti di convegno|