Re: Deep inference and speed-up in proof search

At 9:24 +1000 18.8.04, Rajeev Prabhakar Gore wrote:
> I am still not back in Canberra and am reading this via a browser but the
> notion you seem to need is that CoS polynomially simulates LK but not vice
> versa. A class of interesting formulae may be D'Agastino's class from [MD]
> which shows that KE polynomially simulates LK but not vice versa (or some
> tweeking of this class suited for CoS).
>
> [MD] Mondadori and D'Agostino, "The taming of the cut", JLC 1994 (but the
> date could be wrong).

Hi Raj,

we know already that CoS polynomially simulates LK; actually, I was 
implicitly assuming this in my email. I should have mentioned it.

The idea is very straightforward: just do in CoS what you would do in 
LK. In CoS you have deep inference, but you're not obliged to use it, 
you can use system KS exactly as you would use LK, in a shallow way 
and by keeping branches in a big external conjunction. The only thing 
to check is that the `and' rule can be simulated by switch in 
constant time, but this is entirely straightforward.

By the way, this also addresses a common concern: the big 
nondeterminism in the proof search space. If you do what LK would do, 
you have the same amount of nondeterminism. In fact, there are 
several possible complete strategies one can use in CoS, not just 
one. If you use a certain strategy, you would get the proof search 
complexity associated to that strategy.

For example, you can think of LK as a strategy inside CoS. You can 
also take a system which only generates uniform proofs and use that 
as a strategy inside CoS. You can use resolution as a strategy (what 
you can't do in the sequent calculus); and so on.

To summarise: the fact that deep inference allows for shorter proofs 
than the sequent calculus, doesn't automatically imply that you have 
to pay a price in terms of proof search complexity. The fact that 
many different strategies are available `under the same roof' 
actually leads to much lower *overall* complexity, also taking into 
account search complexity. It's time to write something about this 
stuff...

Anyway, the paper you suggested is very interesting. I didn't know it 
and inside it I found the surprising fact that truth tabling is more 
efficient than tableaux in certain cases! So, I tried in CoS and I 
saw that we can polynomially simulate truth tabling as well. It looks 
like CoS is then at least as efficient as every other system, and 
exponentially better in many cases. Paola and I decided to write a 
paper about this.

Ciao,

-Alessio