Résumé de séminaire

Résumé :

Étant donné un système de preuve S, on peut se poser la question : "S a-t-il un fort contenu algorithmique ou pas ?" selon au moins deux points de vue.

1) Selon le premier point de vue, on dira que S a un fort contenu algorithmique si les règles d'inférence de S induisent naturellement des algorithmes de recherche des preuves. Par exemple, les systèmes à la Hilbert sont pauvres en contenu algorithmique, en ce sens la, par contre, au moins certaines formulations des calculs des séquents de Gentzen sont riches.

2) Selon le deuxième point de vue, on dira que S a un fort contenu algorithmique si les règles d'inférence de S sont telles que la "normalisation" des preuves coïncide avec l'évaluation de programmes associés aux preuves. L'exemple classique de système de preuve ayant un fort contenu algorithmique en ce deuxième sens est la déduction naturelle (Gentzen) pour la logique intuitionniste, grâce à l'isomorphisme dit de "Curry-Howard".

Dans mes recherches, j'ai touché plusieurs domaines (tout en privilégiant les Bases de Données comme champ d'application), mais un fil rouge lie tous mes travaux : l'attention constante au contenu algorithmique des systèmes de preuves, dans les deux sens cités, mais surtout selon le premier des deux. En effet, j'ai beaucoup étudié les problèmes liés à l'automatisation de la recherche de preuves pour les logiques dites "modales".

Dans cet exposé, je vais essayer de donner une description rapide de ces travaux, et de détailler surtout l'application de mes résultats au problème de la gestion des contraintes dites "dynamiques" dans les Bases de Données.

Références :

Ma page web : http://www.lri.fr/~serena

Conditions particulières d'accès :

Le bâtiment du CMI étant fermé pour vacances scolaires, il est necessaire d'entrer par le garage du CMI en utilisant un badge. Si on ne dispose pas d'un badge, on peut appeler au telephone un des membres du LIM-Nord qui devraient être là. Par exemple : Amadio 04 91 11 36 14, Durand 04 91 11 36 12, Lugiez 04 91 11 36 23, Phan-Luong 04 91 11 36 15.