Complexité algorithmique des beaux pré-ordres

Les beaux pré-ordres constituent un outil fondamental en logique et en informatique. Ils fournissent l'argument de terminaison dans de nombreux résultats de décidabilité, que ce soit en résolution de contraintes, déduction automatique, analyse de programme. Ce qui est moins bien connu est que, au-delà de la décidabilité, ces usages ont généralement un contenu algorithmique, amenant à des preuves de complexité.

Travaux en commun avec D. Figueira, S. Figueira, S. Haddad et Ph. Schnoebelen.