Subject: Normalisation Control in Deep Inference Via Atomic Flows
Newsgroups: gmane.science.mathematics.frogs
Date: 2007-06-18 06:34:36 GMT (46 weeks, 6 days, 20 hours and 32 minutes ago)
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.