Proof Search in Acyclic Matrix Graphs (Algorithms and Theory of Computing)
Bertram Fronhöfer · Institutional Repositories DataBase (IRDB) · 1998
In [2] 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 procedures to the just mentioned logics.In this paper we establish 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 col\'umns 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 $\mathrm{a}\mathrm{U}$ literals can be.tested incrementaUy.