LSV Seminar
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.
Past Seminars
Proof complexity of deep inference: past, present and future
- 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.