About | Study | Members | Projects | Publications | Events | Search | Internals | Contact & Imprint

**Course title:** Introduction to Deep Inference and
Proof Nets

**Lecturer:**
Dr. Paola Bruscoli,
Dr. Lutz Strassburger

**Module:** IT

**Status:** advanced unit

**SWS** (lecture/tutorial/practical): 1/0/0

**Credit points:** 1

**Examination method:** written examination

**Prerequisites:** aquaintance with the basics of
propositional classical logic

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:

- New normal forms and decomposition theorems, available thanks to deep inference, provide a richer proof theory;
- 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.

- Kai Bruennler: "Deep Inference and Symmetry in Classical Proofs", PhD-Thesis
- Kai Bruennler and Alwen Tiu: "A Local System for Classical Logic", LPAR'01
- 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 Strassburger: " Linear Logic and Noncommutativity in the Calculus of Structures", PhD-Thesis
- Lutz Strassburger: " A Local System for Linear Logic", LPAR'02
- Lutz Strassburger: "Proof Nets and the Identity of Proofs", ESSLLI'06 lecture notes

- The course web page
- The course will be held from 17th to 21st December.