Les règles logiques sont des fractions

Une règle logique s'écrit traditionnellement sous forme d'une fraction, avec les hypothèses "au numérateur" et la conclusion "au dénominateur".
Nous allons voir qu'en fait une règle logique est bien une fraction, mais avec la conclusion au numérateur et les hypothèses au dénominateur. 
Pour voir cela on utilise la notion catégorique de fraction,  qui généralise la notion usuelle. 
A partir de cette remarque, on obtient un cadre algébrique simple et puissant pour parler de logiques et d'homomorphismes de logique.
Ces résultats ne sont pas récents : ils ont été obtenus avec C. Lair en 2002, mais je trouve qu'ils mériteraient d'être mieux connus. 
Si le temps le permet je parlerai aussi de notre motivation, liée à l'automatisation de preuves concernant des programmes non fonctionnels.
Ce travail entre donc dans le cadre de la correspondance de Curry-Howard-Lambek entre catégories, logique et informatique.