Courses in Winter Term 2007/08 - Introduction to Deep Inference and Proof Nets

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

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:

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.

References

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

Additional Information:

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