Richard McKinley:
Path breaking and analyticity in proof nets

Atomic flows are a new approach to proof transformation due to
Guglielmi and Gundersen;  it has been used to define  new normal forms
for proofs in deep inference formalisms, and guides the design of
algorithms yielding those normal forms. The atomic flow of a
derivation is a graph indicating the flow of atoms in a derivation, as
they are created, destroyed and duplicated.

A striking property of the atomic flow approach is its modularity.
While atomic flows are not themselves derivations, the operations of
normalization are first defined on them, and then shown to be liftable
to a deductive system.  It would be particularly appealing if the same
basic reduction mechanism could be applied to many deductive systems,
but so far lifting has only been shown for deep inference systems.  In
this talk, I will demonstrate how the path-breaker, a particularly
simple reduction on atomic flows, can be lifted in a very intuitive
way to a class of proof-nets for classical logic.  The notion of
normality obtained is weaker than cut-freeness; we will discuss in
what sense such proofs are analytic.