Introduction to Deep Inference and Proof Nets

Paola Bruscoli (University of Bath)

Lutz Straßburger (INRIA Futurs and LIX)

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.

Coursework Exercises and Solutions

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

See the ICCL webpage.

• Kai Brünnler: "Deep Inference and Symmetry in Classical Proofs", PhD-Thesis
• Kai Brünnler and Alwen Tiu: "A Local System for Classical Logic", LPAR'01
• Paola Bruscoli and Alessio Guglielmi: "A tutorial on proof theoretic foundations of logic programming"
• Paola Bruscoli and Alessio Guglielmi: "On the Proof Complexity of Deep Inference"
• Alessio Guglielmi: Webpage on "Deep Inference and the Calculus of Structures"
• Alessio Guglielmi: "A System of Interaction and Structure", ACM Transactions on Computational Logic, 2007
• Lutz Straßburger: "Linear Logic and Noncommutativity in the Calculus of Structures", PhD-Thesis
• Lutz Straßburger: "A Local System for Linear Logic", LPAR'02
• Lutz Straßburger: "Proof Nets and the Identity of Proofs", ESSLLI'06 lecture notes