Linear logic in a refutational setting

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.