The course will give a basic introduction to deep inference, which is a design principle for proof formalisms in which inference rules can be applied at any depth inside the proof. In this course, we will provide a clear understanding of the intuitions behind deep inference, together with a rigorous account of the properties that deep inference proof systems enjoy, especially in regards to normalisation. Properties that particularly stand out are atomicity, locality, and regularity. Normalisation procedures specific to deep inference allow for new notions of normal forms for proofs, as well as for a general modular cut-elimination theory. Furthermore, the ability to track every occurrence of an atom throughout a proof allows for the definition of geometric invariants with which it is possible to normalise proofs without looking at their logical connectives or logical rules, obtaining a purely geometric normalisation procedure.
This course is intended to be introductory. That means no prior knowledge of proof theory is required. However, the student should be familiar with the basics of propositional logic.