Polygraphes, réécriture et logique (Attention : 14h)


Yves Guiraud, . 9 février 2006 14:00 limd 2:00:00
Abstract:

Dans cet exposé, je présenterai la structure de polygraphe, une sorte de complexe cellulaire, à travers ses liens avec la réécriture et la logique. Dans la première partie, nous verrons comment tout système de réécriture de termes peut être traduit sous la forme d'un polygraphe, vu ici comme un système de réécriture de circuits. Sur un exemple, je montrerai comment construire des ordres de terminaison adaptés à ces objets. Dans la seconde partie, nous traduirons le calcul propositionnel et ses démonstrations en un polygraphe : cela permet d'obtenir des représentations bidimensionnelles pour les formules et tridimensionnelles pour les démonstrations. Enfin, si le temps le permet, je parlerai d'une piste menant à une autre description polygraphique des démonstrations classiques, toujours en trois dimensions.