Re: Deep inference and speed-up in proof search

Hello Raj,

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.

Of course, there's no point in `changing notation' unless an 
advantage is obtained. The work we just started shows that deep 
inference provides for exponential speed-ups in benchmark problems, 
so I'd say there's some well founded hope for tuning up new, more 
efficient search strategies than existing ones.

One point to keep in mind is that KE, for example, is a single, 
specific deductive system based on a neat but limited trick (limited 
by shallow inference, I mean). CoS is instead a formalism where you 
can design deductive systems with the greater freedom provided by 
deep inference. This doesn't mean that CoS will be successful, only 
that the analogy is not fair.

In addition, it might be the case that competing against a well 
established technology like tableaux is difficult simply because of 
the inertia associated to a big mass. So, could very well be that CoS 
is a betamax, i.e., superior but not adopted (but superior!). We'll 
see.

Ciao,

-Alessio


At 10:01 +1000 30.8.04, [email protected] wrote:
>Hi Alessio,
>
>okay, great. But I suspect that actual proof search in CoS will still
>be problematic. For many years Marcello wondered why KE was not
>becoming the standard tableau calculus for automated reasoning, given
>his result that traditional tableau cannot even p-simulate truth
>tables. The problem is that the linear KE rule is not local since it
>requires us to find an A and a (~A \/ B) on the current branch in
>order to deduce B. That is, it requires us to find a connection
>between two formulae on the same branch. Alternatively, it requires
>astute applications of cut to get the minor premisses on the branch in
>the first place. Ian Horrocks' experience shows that the ability of a
>calculus to have short proofs is not enough to obtain a good theorem
>prover. Somehow, the dumb tableau method with a few tricks like
>simplification and clever caching seems to do the trick. I am happy to
>be proved wrong, but I suspect that CoS will suffer from the same
>problem.
>
>all the best,
>Raj