Workshop on
EFFICIENT AND NATURAL PROOF SYSTEMS
University of Bath
14-16 December, 2015

The Mathematical Foundations group at the Department of Computer Science, University of Bath, will host a 2.5-day workshop on structural proof theory, starting in the afternoon of 14 December, preceded by a short course on deep inference in the morning of 14 December.

The workshop will focus on the various aspects of structural proof theory, including but not limited to the following topics:

Participation

There is no fee or formal registration for the workshop and anyone is welcome to attend. However, at this stage, we ask that anyone who intends to attend informs us as soon as possible (deadline for expression of interest was 20 November) so that we may accordingly plan coffee breaks and social activities.

All enquiries should be made to wenps2015@easychair.org.

The current list of participants is available.

Venue

Room 1W 2.103, University of Bath.

Course on Deep Inference

Change of time: 14 December 11:00 to 13:00.

(Due to the high quality and number of contributions received by the committee, we have decided to replace the previously advertised course on deep inference by an abridged version on the morning preceding the workshop.)

Deep inference is a modern proof theory offering a better understanding of proofs and extending the range of applications of traditional Gentzen proof theory. This course will offer a brief introduction to deep inference.

Programme

Proposed duration of talks: invited talks 40' (+ discussion), regular contributions 25' (+ discussion).

 

Monday, December 14
10:30 -- 11:00 Welcome coffee and cookies
11:00 -- 13:00

Course

Andrea Aler Tubella, Paola Bruscoli, Alessio Guglielmi, Benjamin Ralph (Bath).
Deep Inference - Normalisation and Complexity.

Two-hour mini-course
13:00 -- 14:20 Lunch
14:20 -- 15:10

Session 1:

Norbert Preining (JAIST). Proof theory of projective geometry -- Orevkov's speed up result in strange surroundings Invited talk
15:10 -- 15:30 Coffee Break
15:30 -- 17:00

Sesssion 2:

Arnold Beckmann (Swansea). Hyper natural deduction. Invited talk
Sonia Marin (INRIA and LIX). Focused and Synthetic Nested Sequents

 

Tuesday, December 15
9:00 - 10:30 Session 3: Roy Dyckhoff (St Andrews). Coherentisation for first-order logic. Invited talk
Marco Volpe (INRIA and LIX). Focused Proof Systems for Modal Logic.
10:30 - 10:50 Coffee Break
10:50 - 12:20 Session 4: Alessio Guglielmi (Bath). Designing a Proof System Around a Normalisation Procedure. Invited talk
Andrea Aler Tubella (Bath). A generalised cut-elimination procedure through subatomic logic.
12:20 - 13:40 Lunch
13:40 -- 15:10

Session 5:

 

Michel Parigot (CNRS and PPS). <TBA>. Invited talk
Ben Ralph (Bath). A natural cut-elimination procedure for classical first-order logic
15:10 -- 15:30 Coffee Break
15:30 -- 17:00

Sesssion 6:

Simona Ronchi della Rocca (Torino). Intersection types and implicit computational complexity. Invited talk
Fanny He (Bath). Towards an atomic lambda-mu-calculus.

Social dinner (served at 19:30)

The Chequers of Bath, 50 Rivers St, Bath BA1 2QA

 

Wednesday, December 16
9:00 - 10:30 Session 7: Stefano Berardi (Torino). Game Semantics and the Complexity of Interaction (about a result of Federico Aschieri) Invited talk
Thomas Powell (Innsbruck). Variations on learning: relating the epsilon calculus to proof interpretations.
10:30 - 10:50 Coffee Break
10:50 - 12:20 Session 8: Marc Bagnol (Ottawa). Complexity of MALL proofnets and binary decision trees.
Luca Roversi (Torino). A class of recursive reversible functions. Invited talk
12:20 - 13:40 Lunch
13:40 -- 15:10

Session 9:

 

Tom Gundersen (Red Hat). <TBA>. Invited talk
Björn Lellmann (Vienna). Linear Nested Sequents.
15:10 -- 15:30 Coffee Break
15:30 -- 17:00

Sesssion 10:

Taus Brock-Nannestad (INRIA and Copenhagen). Reconciling two notions of cut-elimination.
Georg Moser (Innsbruck). The Epsilon Theorems: Simple Things Made Simple. Invited talk

 

Childcare

The Department of Computer Science and the University of Bath are committed to a supportive and inclusive working environment. Childcare will be provided to workshop participants and their children if required. If you need this service, please contact us at wenps2015@easychair.org by 20 November.

Accessibility

If you have requests concerning accessibility or dietary requirements, please contact us at wenps2015@easychair.org and we will do all we can to assist.

Organising and Programme Committee

Funding

EPSRC Project EP/K018868/1 Efficient and Natural Proof Systems.

Participants


Course on Deep Inference

Andrea Aler Tubella, Paola Bruscoli, Alessio Guglielmi, Ben Ralph (Bath)
Deep Inference -- Normalisation and Complexity (two-hour mini course)

This is a course for experts in Gentzen proof theory who want to quickly get the basics of deep inference. We know that in Gentzen theory the normalisation options are limited, for example cut elimination for classical logic is not confluent. Moreover, the complexity of analytic proofs can be high, for example Statman tautologies need exponential size analytic proofs. We argue that these problems are due to unnecessary restrictions of proof composition.

Deep inference is nothing else than allowing proof composition by the same connectives used to compose formulae. This simple stipulation has many benefits. In particular, it is extremely simple to obtain confluent cut elimination for classical logic and an exponential speed-up over analytic proofs in the sequent calculus; for example analytic proofs of Statman tautologies only need polynomial size.

More in general, deep inference allows us to break proofs into elementary components of bounded size, a property that we call locality. This way we can use normalisation methods based on topology. We also obtain a much finer control over the complexity of proofs because the various compression mechanisms, such as cut and sharing, can be separated and dealt with independently.

The aim of this course is to introduce these concepts based on six ideas illustrated by examples, as follows:

Introduction

1. Free composition of proofs leads to locality (AG) Notes for 1, 3

Normalisation

2. Cut elimination by splitting and decomposition (AAT)

3. Locality leads to topological control of normalisation (AG)

4. Confluent cut elimination based on experiments (BR)

Complexity

5. Exponential speed-up over Gentzen analytic proofs (PB) Slides for 5, 6

6. Cut and sharing in deep inference vs. the sequent calculus (PB)


Talks

      1.1.2016