Re: Deep inference and speed-up in proof search

>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.

Let me be a bit more specific on this; after an email I've got from 
Kai I see it wasn't clear. So, very briefly this is what Paola and I 
will write in the paper we planned:

We'll be working mainly with KS + fai^, i.e., system KS with the 
addition of the finite choice cut (see the paper Kai and I wrote for 
FOL75; the finite choice cut is an atomic cut where the atom 
introduced must appear in the conclusion). This system has the finite 
choice property (see previous email from me) and is able to 
p-simulate the sequent calculus with cut. The rather obvious 
conjecture is that every reasonable system can be simulated here 
without a complexity penalty. (BTW: a *shallow* finite choice cut is 
of course enough, and this is beneficial for nondeterminism.)

For example, here is a way to simulate truth-tabling: Let S be a 
formula where propositional variable a appears. Consider the 
following derivation, where, e.g.,  S/-a <- t/ indicates structure S 
where -a is replaced by t everywhere:

        (S/-a <- t,a <- f/,S/a <- t,-a <- f/)
    w_* -------------------------------------
               (S/-a <- t/,S/a <- t/)
    {s,ai_}* ---------------------------
             ([S,a,...,a],[S,-a,...,-a])
         c_* ---------------------------
                   ([S,a],[S,-a])
             2 x s --------------
                    [S,S,(a,-a)]
               fai^ ------------
                       [S,S]
                    c_ ----- .
                         S

By repeating the construction the obvious way, one p-simulates truth 
tabling. Just an example.

Anyway, the points we want to make are:

- KS + fai^ is a *universal* deduction system for propositional 
logic, in the sense that (almost?) every deduction system can be 
p-simulated into it *in a natural way*.

- KS + fai^ has the finite choice property, so it's automatisable.

After these very basic points are established, we will argue that in 
KS + fai^, thanks to deep inference, much shorter proofs are 
available than in other systems, and that in many cases the 
nondeterminism can be greatly reduced.

For example, it is possible to get rid of fai^ and still be able to 
prove Statman's tautologies in polynomial time, what no system I know 
of can do without something equivalent to a cut rule.

Conclusion: deep inference is the natural setting where to look for 
short proofs without having to cope with greater nondeterminism than 
usual.

Further conclusion: we provide another argument in favour of not 
being obsessive about eliminating cut, in accordance to Boolos, 
Smullyan and Mondadori-D'Agostino, and I guess many other people.

As you see, this is going to be an easy paper, but we think it's time 
somebody writes down all this stuff in a clear way. Depending on the 
result, we might want to adjust marketing accordingly, for example we 
might decide to deemphasise the sequent calculus as our main 
reference point.

Please note that many interesting conjectures won't be touched by 
this paper. For example, take pigeonhole. We know already that it can 
be proved polynomially by the sequent calculus with cut. This result 
is transferred immediately to KS + fai^, but then the interesting 
problem remains open of *whether fai^ is necessary*. In other words, 
it might be possible to prove pigeonhole *without* fai^. Doing this 
would be a very nice and interesting stunt (I guess Lutz has ideas 
about that), but it's overkill for the kind of argument we want to 
make.

Ciao,

-Alessio