In [Fro96] we gave a characterization of theoremhood in terms of the Connection Method for the multiplicative fragments of Affine (Contraction-Free) and Linear Logic. Such matrix characterisations constitute a basis for the adaption of the classical path checking proof search procedures to the just mentioned logics.

Based on this work we present computationally advantageous variants of the previously developed matrix characterisations. Instead of the complementarity of paths they hinge on the total connectedness of a sufficient number of virtual columns in a matrix (non-purity).

From these refined matrix characterisations we derive a pruning technique for proof search in acyclic (and linear) matrix graphs, which can be used for multiplicative Affine Logic. Extending proof search to multiplicative Linear Logic, we show that the additionally required minimality of spanning sets is assured by depth-first search, and that the necessary connectedness of all literals can be tested incrementally.

[Fro96] B. Fronhöfer:
The Action-as-Implication Paradigm: Formal Systems and Application. CSpress, München 1996, Germany.