A survey of proof nets and matrices for substructural logics

TL;DR

This survey compares matrix methods and proof nets across substructural logics, introducing a new proof net approach for nonassociative Lambek systems and providing a unified notation for comparison.

Contribution

It offers a comprehensive overview of proof schemes for substructural logics, including a novel proof net treatment for nonassociative Lambek logic and a unified notation for comparison.

Findings

Unified notation facilitates comparison of proof schemes

Novel proof nets for nonassociative Lambek logic introduced

Survey covers a range of substructural logics from classical to nonassociative

Abstract

This paper is a survey of two kinds of "compressed" proof schemes, the \emph{matrix method} and \emph{proof nets}, as applied to a variety of logics ranging along the substructural hierarchy from classical all the way down to the nonassociative Lambek system. A novel treatment of proof nets for the latter is provided. Descriptions of proof nets and matrices are given in a uniform notation based on sequents, so that the properties of the schemes for the various logics can be easily compared.