Vendredi 21 Octobre


Retour à la vue des calendrier
Vendredi 21 Octobre
Heure: 11:00 - 12:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Some interplays between proof theory and computational complexity
Description: Anupam Das Proof complexity is the branch of proof theory concerned with the size of proofs. Due to old and well-known results of Cook and Reckhow, many important questions about computational complexity are equivalent to natural problems in proof complexity. For instance, coNP = NP just if there is an 'efficient' proof system for classical propositional logic. I will survey a now well-developed line of work on the proof complexity of 'deep inference' systems which has culminated in several novel phenomena in proof complexity, including improved bounds for monotone proof systems. I will also discuss remaining open problems in the area and some of their consequences.

A closely related area to proof complexity is bounded arithmetic, which studies weak fragments of arithmetic whose representable functions are typically feasible complexity classes, via bounds on quantifiers. They also act as uniform versions of corresponding propositional systems, forming a three-way correspondence. I will show how this methodology can be extended to certain deep inference and monotone systems via intuitionistic versions of bounded arithmetic, making use of a novel technique that combines the usual 'witness function method' of bounded arithmetic with realisability style extraction. I will further motivate the study of such theories in 'linear logic' in order to address the remaining correspondences, and present some recent work along this line.

Finally I will present an upcoming research project that aims to unify various strands of this research in order to develop a comprehensive approach to monotone complexity classes.