The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.

The seminar is open to public and does not require any form of registration.

- Date
- Wednesday, December 09 2015 at 02:30PM
- Place
- Amphi A 117 (Bat. Alembert)
- Speaker
- Anupam Das (ENS Lyon)

In this talk I will survey the current state of research on the complexity of deep inference proofs in classical propositional logic, and also introduce a program of research proposing to further develop this subject.

Deep inference calculi, due to Guglielmi and others, differ from
traditional systems by allowing proof rules to operate on *any*
connective occurring in a formula, as opposed to just the main
connective. Consequently such calculi are more fine-grained and admit
smaller proofs of benchmark tautologies, including the pigeonhole
principle. As well as plainly theoretical motivations, this is
advantageous from the point of view of proof communication, allowing
for compact and easy-to-check certificates for proofs.

I present a graph-based formalism called 'atomic flows' and a rewriting system on them that models proof normalisation while preserving complexity properties. I show how such an abstraction has been influential in work up to now, allowing the obtention of surprisingly strong upper bounds and simulations in analytic deep inference.

The biggest open question in the area is the relative complexity
between the minimal system KS and a version that allows a form of
sharing, KS+. To this end I will introduce a novel approach using weak
fragments of arithmetic to serve as uniform counterparts to these
nonuniform propositional systems, inspired by the approach of *bounded
arithmetic*. As well as associating a propositional system with an
arithmetic theory in a formal sense, this also naturally identifies an
associated complexity class of functions, and so tools and intuitions
from logic and complexity theory can thence be used to obtain more
powerful results in proof complexity.

Due to the peculiarities of deep inference calculi, the search for corresponding arithmetic theories takes us into the unexplored territories (from the point of view of bounded arithmetic) of intuitionistic and substructural logics, requiring an interesting interplay of subjects at the interface of logic and computation.