Re: Deep inference and speed-up in proof search

Hi Alessio,

> I don't understand your concerns about CoS's proof search. Just take
> any complete proof search strategy (Gentzen's LK, resolution, ...)
> and express it in CoS. It's just a change of notation, proof search
> doesn't change a bit, so CoS is no worse than any other formalism.

But that is precisely my point. Suppose you take Gentzen's LK and
implement its search strategy inside CoS. So CoS is now complete.

Your p-simulation result will say something like:
  for every derivation in traditional LK
  there is a (at most polynomially longer) CoS derivation

Your result does *not* say that the said CoS derivation can be found
using the LK strategy, only that a CoS derivation exists. 

Question: given an arbitrary LK-derivable sequent, how will you find
the short(er) CoS derivation of *this* sequent ?

It is highly unlikely that any one search strategy is going to work
for every LK-derivable sequent.

Similarly, we know KE p-simulates LK, but nobody uses KE because in
the average case, it does worse *in practice*. That is, there is a
shorter KE derivation, but the search space needed to find it is
larger!

It seems to me that you are confusing existence of shorter derivations
with the size of the search space. 

Ciao,
Raj