Un formalisme pour réduire la taille des preuves




Date(s) : 20/11/2014   iCal
11 h 00 min - 12 h 00 min

La deep inference est un formalisme des preuves généralisant le calcul des séquents. Il permet d’exprimer plus de logiques d’une façon plus compacte. Je passerai en revue ses principales propriétés aux travers de la logique BV, la logique classique et les atomic flows. J’aborderai également les récentes tentatives de définir la substitution d’un atome par une dérivation en deep inference.

[http://www.bath.ac.uk/comp-sci/research/mathematical-foundations/]

Catégories Pas de Catégories



Retour en haut