We present a demonstration of Andreoli’s focusing theorem for proofs of linear logic (MALL) that avoids directly reasoning on sequent calculus proofs. Following Andreoli-Maieli’s strategy, exploited in the MLL case, we prove the focusing theorem as a particular sequentialization strategy for MALL proof nets that are in canonical form. Canonical proof nets satisfy the property that asynchronous links are always ready to sequentialization while synchronous focusing links represent clusters of links that are hereditarily ready to sequentialization.

Maieli, R. (2022). A Proof of the Focusing Theorem via MALL Proof Nets. In Logic, Language, Information, and Computation (pp.1-17). Springer Cham [10.1007/978-3-031-15298-6_1].

A Proof of the Focusing Theorem via MALL Proof Nets

Maieli, Roberto
2022

Abstract

We present a demonstration of Andreoli’s focusing theorem for proofs of linear logic (MALL) that avoids directly reasoning on sequent calculus proofs. Following Andreoli-Maieli’s strategy, exploited in the MLL case, we prove the focusing theorem as a particular sequentialization strategy for MALL proof nets that are in canonical form. Canonical proof nets satisfy the property that asynchronous links are always ready to sequentialization while synchronous focusing links represent clusters of links that are hereditarily ready to sequentialization.
978-3-031-15297-9
Maieli, R. (2022). A Proof of the Focusing Theorem via MALL Proof Nets. In Logic, Language, Information, and Computation (pp.1-17). Springer Cham [10.1007/978-3-031-15298-6_1].
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/418223
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact