Re: Deeper Cuts in Deep Inference

Hi Bruno,

> In fact, I think that some of the most efficient decision procedures
> nowadays already use a lot of deep inference. People like to think of
DPLL
> and CDCL as particular strategies for shallow resolution proof search,
but
> things like unit propagation and "decisions" might be more easily
> understood as a combination of macro-switches and (co)contractions,
moving
> some literals outside the clauses and stacking them on a context for the
> clauses...

It is always possible to add sound and invertible rules to your system to
make it more efficient. However, the main issue here is to achieve
'efficiency' in proof search while preserving as many properties as
possible from those such as modularity, locality, atomicity, symmetry and,
of course, cut-elimination. Splitting technique provides some insight into
this, but in the general setting, this is difficult.

Best regards,
Ozan