An introduction to deep inference

ESSLLI 2019 Course — 1st Week (5-9 August) — 9:00-10:30

Andrea Aler Tubella & Lutz Straßburger

Overview

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.



Course notes are online here!



Tentative syllabus

Five 90-minute lectures are split into ten 45-minute units.

Links

Main ESSLLI 2019 webpage

ESSLLI 2019 webpage for this course

Deep inference webpage maintained by Alessio Guglielmi