Compact representation (left) of an equivalence class of proofs (right)
Compact representation (left) of an equivalence class of proofs (right)
This course provides an introduction to the techniques and methods proper of deep inference, a recent methodology in proof theory that has been developed for the past 15 years. Purpose of the course is to provide participants with a detailed and compact presentation of the many features that deep-inference based proof systems exhibit. Through small examples and exercises mixed with usual presentations our aim is that of developing an initial technical understanding of deep inference, while simultaneously highlighting, through examples, the different scope of applicability of more traditional methods.
This course is mainly about understanding normalisation in proof theory by uncovering its local and geometric nature. We will use the tools of deep inference, which we could succinctly describe as an extreme form of linear logic. By doing so, we obtain a better proof theory than the traditional one due to Gentzen: we can provide proof systems for more logics, with smaller proofs, less syntax, less bureaucracy and we have a chance to make substantial progress towards a solution to the century-old problem of the identity of proofs.
Slides: handout, strip-tease
20.8.2015 Alessio Guglielmi email
