Un formalisme pour réduire la taille des preuves
Date(s) : 20/11/2014 iCal
11h00 - 12h00
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
