Rémy Malgouyres (GREYC)

Cet exposé présente quelques liens entre la logique et la complexité algorithmique. On introduit d’abord beaucoup d’exemples de formulations logiques, portant essentiellement sur des problèmes de graphes, dans le but de cerner quels types de problèmes s’expriment ou ne s’expriment pas dans les logiques du premier ordre ou du second ordre; on verra quelles conclusions on peut en tirer concernant la complexité des divers problèmes étudiés.

Enfin, de façon plus fine, on s’intéresse aux problèmes calculables en temps linéaire. A l’aide de la logique, on montre que non seulement beaucoup de propriétés de graphes - connectivité, biconnectivité, nonplanarité - sont décidables (par des algorithmes astucieux) en temps linéaire O(e+n) où e et n désignent le nombre d’arêtes et le nombre de sommets du graphe, mais aussi que ces propriétés sont vérifiables en temps non déterministe O(n), donc linéaire en le nombre de sommets, c’est à dire avec une preuve sous-linéaire (en la taille du graphe), donc encore plus courte que leur calcul déterministe (résultats récents communs avec C. Lautemann et S. Ranaivoson: projet Procope Caen-Mayence).