Normalisation Control in Deep Inference Via Atomic Flows

Hi,

We would like to announce a nice paper about normalisation. Comments
are welcome.

<http://cs.bath.ac.uk/ag/p/NormContrDIAtFl.pdf>

Regards,

Tom



Normalisation Control in Deep Inference Via Atomic Flows

Alessio Guglielmi and Tom Gundersen

Abstract:

We introduce diagrams, called 'atomic flows', that forget much of the syntactic
structure of derivations and only retain causal relations between
atoms. Using atomic
flows on propositional logic, we can design and control several
normalisation procedures.
In particular, we can obtain cut elimination as a special case of more
general normal
forms. This technique only relies on substituting derivations in the
place of atoms,
similarly to natural deduction, and not on permuting inference steps,
as in the sequent
calculus. Because they abstract away from most syntactic details,
atomic flows allow for
very simple control of normalisation procedures, which would be
otherwise cumbersome
in the bare syntax. We operate in deep inference, a very general
methodology, where
normalisation is more difficult to control than in other syntactic paradigms.