Introduction to Deep Inference and Proof Nets

Dresden, December 17-21, 2007


Paola Bruscoli (University of Bath)

Lutz Straßburger (INRIA Futurs and LIX)

Course description

The course is intended to be an introduction into the venerable field of proof theory via the novel concepts of deep inference and proof nets. Deep inference can be understood as a principle for designing a deductive system for a logic. It is based on the idea of rewriting a formula inside arbitrary contexts, which is alien to other formalisms like sequent calculus. On the other hand, proof nets are a graph like presentation of formal proofs. The basic idea is to abstract away from unrelevant syntactic "bureaucracy" that is usually involved in deductive systems. Deep inference and proof nets do not solely give new insights into traditional results of proof theory, like cut elimination, rather they overcome traditional methodologies in at least the following respects:

  1. New normal forms and decomposition theorems, available thanks to deep inference, provide a richer proof theory;
  2. Some logics, motivated by modern computer science, that cannot be treated in traditional proof theoretical methodologies, find in deep inference a natural setting for being studied.

Course Material for Students

Coursework Exercises and Solutions

Handout for Lecture 1
Handout for Lecture 2
Handout for Lecture 3
Handout for Lecture 4


See the ICCL webpage.