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.

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 [10.4230/LIPIcs.FSCD.2016.20].

Computing connected proof(-structure)s from their Taylor expansion

TORTORA DE FALCO, LORENZO
2016-01-01

Abstract

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.
978-3-95977-010-1
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 [10.4230/LIPIcs.FSCD.2016.20].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11590/311742
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 13
  • ???jsp.display-item.citation.isi??? ND
social impact