Workshop: Twenty Years of Deep Inference

Oxford, 7 July 2018


Deep inference is paradigm for designing deductive proof systems. The inference rules in such systems can perform arbitrary rewriting inside formulas. This is very different from what one would expect from more traditional formalisms, like sequent calculus or natural deduction, where formulas are always decomposed along their main connective.

On one side, this provides much more freedom in the design of proof systems, and on the other side this causes a massive breakdown of all important proof theoretical results. Consequently, the early reasearch in deep inference went into reestablishing traditional results, like cut elimination, that one would expect from a deductive proof system.

After that many new results for deep inference have been obtained in recent years, in particular:

Besides that, deep inference inspired new notions of proof nets and semantics for proofs, and new research in proof complexity.

The purpose of this workshop is to present this vast growing field in a coherent, easy accessible way to other communities in all areas of logic in computer science, and bring together researchers in the area of deep inference to exchange ideas and to discuss their current work.

An up-to-date bibliography on deep inference can be found here.

Invited Speakers

Alessio Guglielmi (University of Bath)
Willem Heijltjes (University of Bath)






The workshop is part of FLoC 2018.


Andrea Aler-Tubella
Lutz Straßburger