Re:Deeper Cuts in Deep Inference

Hi Bruno,

If I'm not mistaken, the three rules that you propose are, as you 
say, all derivable via switches and cuts (in the sense of SKS cuts 
ai^). They could be further generalised to generic formulae (instead 
of atoms), and still be derivable via switches and cuts.

Conversely, ai^ is an instance of your rules, of course.

As you say, the difference is in the bureaucracy of the proofs: your 
rules are friendlier from the point of view of proof search. However, 
the vanilla ai^ rule seems more manageable and more fundamental for 
investigating normalisation.

It's perhaps interesting to note that all the bureaucracy disappears 
when one turns to atomic flows [1]: all these rules generate the same 
atomic flows. However, we are still far from being able to use atomic 
flows for proof search (it's an open problem whether atomic flows are 
a proof system).

Ozan Kahramanogullari has done extensive work on the design of 
proof-search friendly proof systems, I think all his papers are 
accessible from the deep-inference web page (please let me know if 
anything is missing) [2]. I think it would be interesting to continue 
Ozan's investigation, because there are exponentially shorter 
cut-free proofs in deep inference than in the sequent calculus [3].

Of course, one problem is that the proof-search nondeterminism in 
deep inference seems to be, at first sight, huge and impractical. 
However, it might turn out that eventually deep inference will have 
less nondeterminism than the sequent calculus, because of two recent 
developments:

1) The deep-inference formalism of open deduction eliminates quite a 
lot of bureaucracy in proof construction, and compares favourably to 
the sequent calculus [4].

2) There's a recent result by Anupam Das (still not on the web, as 
far as I know) [5] that shows that in order to access the 
exponentially shorter proofs that I was mentioning above, a very 
small degree of deep inference, just above the sequent calculus, is 
sufficient.

In conclusion: I would expect that some carefully designed cut rules 
like the ones you propose, inside an open-deduction proof system with 
very limited deep inference could make for an excellent proof system 
for proof assistants.

That's all I can think of (in Italy we say: `partire per la tangente').

Ciao,

-Alessio

[1] <http://tel.archives-ouvertes.fr/docs/00/50/92/41/PDF/thesis.pdf>
     <http://www.lmcs-online.org/ojs/viewarticle.php?id=341>
     <http://www.lix.polytechnique.fr/~lutz/papers/AFII.pdf>

[2] <http://alessio.guglielmi.name/res/cos/#LD>
     <http://alessio.guglielmi.name/res/cos/#IM>

[3] <http://cs.bath.ac.uk/ag/p/PrComplDI.pdf>

[4] <http://drops.dagstuhl.de/opus/volltexte/2010/2649/>

[5] 
<http://www.bath.ac.uk/comp-sci/people/contact/index.php?contact=Mr_Anupam_Das>


At 15:17 -0300 15/3/11, you wrote:
>Hi!
>
>I noticed that in deep inference (I am having the system SKS in 
>mind), the cut is not as "deep" as it could be. What I mean is the 
>following:
>
>consider the "ai-up" (a.k.a. cut) rule of SKS:
>
>S{~a and a}
>----------------
>S{ false }
>
>This rule is certainly deep in the sense that it can be applied 
>inside any context S. But it is also shallow in the sense that the 
>cut-formulas do not appear inside any context. I can imagine a 
>"deeper" cut-rule as follows:
>
>S{~a and S'{a}}
>--------------------  (1)
>S{ S'{false} }
>
>and we could go further and have something like this (which is like 
>a deeper application of modus ponens):
>
>S{(~a or b) and S'{a}}
>------------------------------  (2)
>S{ S'{b} }
>
>and we can try to go even further and find out what happens when 
>both cut-formulas are within arbitrary contexts:
>
>S{S''{~a} and S'{a}}
>-------------------------------------------------------------------------- 
>(3)
>S{ ?? }    (any of S{S'{S''{false}}} or S{S''{S'{false}}} ???)
>
>
>I think that deep modus ponens as formalized by the inference rule 
>(2) above is a quite natural reasoning pattern. I use it all the 
>time, and I think we can also say that theorem provers implicitly 
>use it whenever they are doing deep replacements during, for 
>example, skolemization.
>
>I guess both (1) and (2) could be simulated in SKS by several 
>applications of the switch rule followed by an application of 
>"ai-up", but this would be quite bureaucratic, in my opinion.
>
>Anyway, these are some things that came to my mind while developing 
>a proof format for an SMT-solver (that does skolemization as a 
>pre-processing step), and I haven't thought much about this yet. So, 
>if you have any comments (e.g. whether it has already been 
>investigated somewhere, whether I am out of my mind and it doesn't 
>make sense to investigate it for some reason,...), please let me 
>know...
>
>Best regards,
>
>Bruno