Long ago, I ran into a thing called "cancellative Linear Logic" or something like that, where the operators "par" and "times" are blurred. Can anyone give me pointers about that. Thanks. Jean-Marc Jean-Marc Andreoli | Tel: +33 76 61 50 80 (direct) Rank Xerox Research Center | +33 76 61 50 50 (switchboard) 6 Chemin de Maupertuis | Fax: +33 76 61 50 99 38240 Meylan (France) | E-mail: Jean.Marc.Andreoli@xerox.fr