Re: Deep inference and speed-up in proof search

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