Re: Nondeterminism

Hi,

> In other words: given, say, a propositional
> classical logic formula and CoS system KS, one
> can say: `yes, if I take KS at face value I have
> a huge nondeterminism, but I can simply use KS as
> I would use LK in the sequent calculus: this
> gives me a complete strategy which trims out a
> huge portion of the search space.' Of course,
> going this way might mean losing the opportunity
> of finding very short proofs, but that's life,
> and anyway the point is taken that suffering from
> excess of nondeterminism is not the case.
>

A short note: system DKS does exactly this by simulating
G3 in the calculus of structures. This way proof search
becomes deterministic computation. However, I believe,
because of deep inference applicability of the
distributivity rule deeply provides shorter proves than
those of G3. Of course, in the worst case, e.g., pigeon
hole, there is an exponential blow up in the width of the
proofs, as in G3, because of the implicit contraction due
to distributivity rule.

There is note on this and a Maude module that implements
DKS with respect to a strategy at the Implementations web-site.

http://www.informatik.uni-leipzig.de/~ozan/maude_cos.html

Cheers.
-Ozan