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-01-01
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
