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
