## Interpolants and Dynamics of Cut-elimination

- DIMACS Center - Room 431
- Busch Campus
- Piscataway, New Jersey
- April 26, ** 1:30 ** p.m.

### Abstract:

We consider the Craig Interpolation Theorem for the propositional
sequent calculus _with_ cuts (which is polynomially equivalent to Frege
Systems) and we look at tautologies A(p_1,..., p_n) -> B(q_1, ... , q_k)
where A and B do not have variables in common.
We know that either A-> or ->B is a provable sequent and we ask whether
there is a proof of A-> or a proof of ->B which is polynomially bounded
in the original proof of A->B.
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'.)