For cut-free proofs the answer is positive but for proofs with cuts the question is open. The difficulties seem to lie in the dynamics of the procedure of cut-elimination. The talk will be dedicated to the analysis of the dynamical properties of the unwinding of a proof with cuts into a proof without cuts.
The results we will present are based on an analysis of graphs associated to proofs (i.e. a finite graph which traces the flow of occurrences of formulas in proofs; this notion has been introduced in [Buss, 1991]. The idea of using the flow of occurrences to study the structure of proofs was present in [Girard, 1987] with the concept of `proof net'.)