
Evènement pour le groupe Séminaire Méthodes Formelles
Date  20200121 07:0007:00 
Titre  Computational content of circular proof systems 
Résumé  Cyclic proofs are a class of formal proof systems that allow some kind of circular reasoning. Unlike classical proofs, represented by finite trees with axioms as leaves, cyclic proofs are represented by trees containing infinite branches. The CurryHoward correspondence allows us to see these cyclic proofs as programs. We investigate the computational content of a cyclic proof system based on Kleene algebra, where we see expressions as data types. Different proofs of the same sequent e  f can be interpreted as different programs mapping every input of type e to an output of type f. We show that depending on the particular rules allowed in the system, the computational content of proofs matches different known complexity classes: regular languages, LogSpace, primitive recursive functions, system T. Various tools are used to pinpoint these different expressive powers, including a newly introduced class of automata (Jumping Multihead Automata), and results from the field of reverse mathematics.
This is joint work with Laureline Pinault, Damien Pous, and Anupam Das. 
Lieu  178 
Orateur  Denis Kuperberg 
Email  https://perso.enslyon.fr/denis.kuperberg/ 
Url  CNRS, ENS Lyon 
Aucun document lié à cet événement. RetourRetour à l'index
 