Re: Decomposition for classical logic

On Tuesday 01 June 2004 14:14, Kai Brünnler wrote:
> What does that mean? Cut elimination should change the net, shouldn't it?
>
> -Kai

What I had in mind is the following:
A proof net for a derivation 

  P
  |
  Q

is a graph that contains the information about P and Q, as well as which 
atoms are erased, duplicated, introduced, etc.

This net then represents at the same time the two different compositions of 
that derivation, as well as the cutfree proof of [-P,Q] , i.e., the 
implication P->Q.

-Lutz