Sequent-style refutation calculi with non-invertible rules are challenging to design because multiple proof-search strategies need to be simultaneously verified. In this paper, we present a refutation calculus for the multiplicative–additive fragment of linear logic (MALL) whose binary rule for the multiplicative conjunction (⊗) and the unary rule for the additive disjunction (⊕) fail invertibility. Specifically, we design a cut-free hypersequent calculus HMALL, which is equivalent to MALL, and obtained by transforming the usual tree-like shape of derivations into a parallel and linear structure. Next, we develop a refutation calculus HMALL based on the calculus HMALL. As far as we know, this is also the first refutation calculus for a substructural logic. Finally, we offer a fractional semantics for MALL—whereby its formulas are interpreted by a rational number in the closed interval [0, 1] —thus extending to the substructural landscape the project of fractional semantics already pursued for classical and modal logics.

### Linear logic in a refutational setting

#### Abstract

Sequent-style refutation calculi with non-invertible rules are challenging to design because multiple proof-search strategies need to be simultaneously verified. In this paper, we present a refutation calculus for the multiplicative–additive fragment of linear logic (MALL) whose binary rule for the multiplicative conjunction (⊗) and the unary rule for the additive disjunction (⊕) fail invertibility. Specifically, we design a cut-free hypersequent calculus HMALL, which is equivalent to MALL, and obtained by transforming the usual tree-like shape of derivations into a parallel and linear structure. Next, we develop a refutation calculus HMALL based on the calculus HMALL. As far as we know, this is also the first refutation calculus for a substructural logic. Finally, we offer a fractional semantics for MALL—whereby its formulas are interpreted by a rational number in the closed interval [0, 1] —thus extending to the substructural landscape the project of fractional semantics already pursued for classical and modal logics.
##### Scheda breve Scheda completa Scheda completa (DC)
2023
Settore M-FIL/02 - Logica e Filosofia della Scienza
Settore MAT/01 - Logica Matematica
Multiplicative-additive linear logic; refutation calculi; hypersequents; fractional semantics
File in questo prodotto:
File
Linear logic in a refutational setting.pdf

Accesso chiuso

Tipologia: Published version
Licenza: Non pubblico
Dimensione 1.29 MB
Linear_logic_refutational_setting_post_print.pdf

Open Access dal 10/08/2024

Tipologia: Accepted version (post-print)
Licenza: Solo Lettura
Dimensione 390.74 kB
Utilizza questo identificativo per citare o creare un link a questo documento: `https://hdl.handle.net/11384/137233`