Re:implementation of system BV

At 14:51 +0200 27.4.05, Ozan Kahramanogullari wrote:
>I would like to advertise an applet which implements
>system BV. It can be found at
>
>http://tom.loria.fr/examples/structures/BV.html

Ozan is too modest. This is an important milestone for us, because it 
shows that the huge nondeterminism inherent in deep inference can be 
won, and elegantly so.

In fact (if I'm not mistaken, correct me if I'm wrong, Ozan) the 
implementation faithfully implements a system that Ozan devised to 
this purpose. What is interesting about Ozan's system is that not 
only it is efficient (while maintaining equivalence to BV), it also 
has cut elimination, so it is a first class proof theory citizen.

All this is explained in a recent paper by Ozan: 
<http://www.informatik.uni-leipzig.de/~ozan/Papers/reducingNondetTR.ps>.

It is important, I think, to keep this in mind when confronted with 
the usual objection that `deep inference has huge non-determinism'.

-Alessio