A General View of Normalisation through Atomic Flows

Atomic flows is a geometric invariant of classical propositional proofs in deep inference. In this thesis, atomic flows are used to describe new normal forms of proofs, of which the traditional normal forms are special cases. Several normalisation procedures for obtaining the normal forms are also given. A new deep-inference formalism called the functorial calculus, which is more flexible than the traditional calculus of structures, is defined and used to present the results. Two surprising results are presented, that proofs can be normalised without looking at their logical connectives or logical rules; and that normalisation can be performed in less than exponential time.

Autorentext

Tom Gundersen studied Mathematics and Computer Science at the University of Bath, where he graduated with a PhD in 2010. After graduating he worked for Institut National de Recherche en Informatique et en Automatique (INRIA) and later Centre National de la Recherche Scientifique (CNRS) in France. He now lives in Paris with his husband John.