11/6/09 Lorenzo Tortora de Falco (Roma)

Sémantique relationnelle et temps d'exécution en Logique Linéaire

Qu'est-ce qu'un calcul correct ? Une tentative de répondre à la question est de donner un maximum de place aux calculs non corrects. On sera alors amené à identifier des propriétés cruciales du calcul, qui seront les témoins de sa correction (terminaison faible ou forte, confluence, exécution en temps borné, etc...). En guise d'introduction, je discuterai du point de vue de la logique linéaire (LL) sur la question, pour prendre ensuite celui de la sémantique relationnelle sur lequel portera l'essentiel de l'exposé. Je présenterai les résultats principaux d'un travail en collaboration avec Daniel De Carvalho et Michele Pagani: 1) un réseau de preuve de LL est normalisable ssi son interprétation ``exhaustive'' est non vide 2) à partir de l'interprétation de deux réseaux sans coupures de LL on peut calculer le nombre exact d'étapes d'élimination des coupures conduisant du réseau obtenu en coupant entre eux les deux réseaux de départ et sa forme normale. Si le temps le permet, je discuterai d'une possible amélioration de ce dernier résultat (travail en cours avec Daniel De Carvalho).