Decidability question

[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

Can some one tell me what is known about the decidability of the
equational theory on proof terms of the (tensor,I,!,-o)-fragment of
intuitionistic linear logic.

The equational theory I have in mind would be one that is sound and
complete for a particular class of models. The class of models I have
in mind are the L-NL models/Linear Categories although I'd also be
interested in the answer for other notions of model.

Also what applications would such a result have (if any!)?



Neil Ghani 

Tel	+33 1 44 32 32 77
Email	ghani@ens.fr
Webress	http://www.ens.fr/~ghani 
Address LIENS-DMI, Ecole Normale Superieure, 
        45 Rue D'Ulm, 75230 Paris Cedex 05, France