Re: Deep inference and speed-up in proof search

Hi Raj,

no, I'm not making any confusion, I do mean that we can do in CoS 
what one can do in the sequent calculus (for example), including 
having a proof search space of the same size. I'll show you a simple 
example below.

My p-simulation result is stronger than you suggest (and completely 
trivial!, at least for the sequent calculus). It says that for every 
system X in the sequent calculus there is a system XS in CoS whose 
proof search space is exactly the same as the one of X, meaning that 
the trees are isomorphic and there is a bijective correspondence 
between every proof (attempt) for XS and every proof (attempt) for X, 
and these objects all have the same size. In other words: it's a 
straightforward isomorphism.

For example, system GS1pS is the following system, trivially obtained 
from GS1p:

         GS1p                   GS1pS
         ====                   =====


         ---         ~>          --- ,
          t                       t

                                  C
        -----        ~>       ---------- ,
        A, -A                 (C,[A,-A])

   Phi, A   Psi, B        (C,[Phi,A],[Psi,B])
   ---------------   ~>   ------------------- ,
    Phi, Psi, A^B         (C,[Phi,Psi,(A,B)])

      Phi, A, B
      ---------      ~>        (nothing) ,
      Phi, AVB

      Phi, A, A              (C,[Phi,A,A])
      ---------      ~>      ------------- ,
       Phi, A                 (C,[Phi,A])

        Phi                     (C,Phi)
       ------        ~>       ----------- .
       Phi, A                 (C,[Phi,A])

As you see, GS1pS is just a trivial change of notation, the external 
conjunction keeps the branches of the tree, and then one looks inside 
disjunctions at level one for sequents. GS1pS has *the same* search 
space of GS1p. Of course, no deep inference is used here, all rules 
are shallow. (And so, using GS1pS would be pointless.)

Suppose now that you want to use a bit of CoS features, for example 
you can add a medial rule to system GS1pS:

   (C,[(A,D),(B,E)])
   ----------------- .
    (C,[A,B],[D,E])

Now the proof search space becomes wider (more rules = more choices), 
but you'll also find shorter proofs. You can also add a deeper 
version of medial, like

   S[(A,D),(B,E)]
   -------------- ,
   S([A,B],[D,E])

and the proof search width becomes even larger but even shorter 
proofs are available; and so on.

On the other hand you can also think about removing rules, and 
trading again width of the search space with length of proofs. Of 
course, one might also think about using heuristics on top of these 
proof search strategies.

The point is that you can play this game with huge freedom in deep 
inference, and you will never go outside of proof theory, meaning 
that you know that there is an underlying system with all the proof 
theoretic properties you can desire. For example, splitting theorems 
give you an immediate property similar to uniform provability which 
is completely impossible in shallow systems. This alone cuts down the 
size of the search space exponentially.

Now, I think it's *very likely* that by playing this trade-off game 
between width of the search space and length of proofs one will find 
an optimal solution which will be much better (and much different) 
than what is available in shallow systems. This, simply because we 
are removing a constraint that goes right in the way of provability.

In fact, it's very intuitive: if you work with formula trees and 
you're always constrained into decomposing them starting from the 
root, you will probably miss precious opportunities. Very likely 
there is information in those trees that should be `put in contact' 
(in an axiom, I mean) immediately, without waiting for the mechanism 
to undo (and perhaps also redo) all the tree structure around the 
information that matters.

Just think of contraction: how much material do you duplicate that 
you then throw away just to duplicate something deeply buried inside 
a formula? If you're not convinced, take a pigeonhole tautology and 
try proving it with SKS, and you'll see what I mean.

Why don't you subscribe to Frogs? <http://alessio.guglielmi.name/frogs>.

Ciao,

-Alessio


At 18:00 +1000 31.8.04, Rajeev.Gore-FCV4sgi5zeUQrrorzV6ljw@xxxxxxxxxxxxxxxx 
wrote:
> 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