Deeper Cuts in Deep Inference

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=