# Intellectics Group: Technical Report 96-17

## Connection-Based Proof Construction in Linear Logic

### Christoph Kreitz and Heiko Mantel and Jens Otten and Stephan Schmitt

We present a matrix characterization of logical validity in the multiplicative
fragment of linear logic. On this basis we develop a matrix-based proof search
procedure for this fragment and a procedure which translates the machine-found
proofs back into the usual sequent calculus for linear logic. Both procedures
are straightforward extensions of methods which were developed for a uniform
treatment of classical, intuitionistic and modal logics. They can be extended
to further fragments of linear logic once a matrix characterization has been
found.