La résolution de contraintes est un problème qui se pose naturellement quand on cherche à étendre des algorithmes de démonstration automatique, comme la résolution ou les tableaux, à des logiques dans lesquelles une théorie est définie par des axiomes et des règles de calcul. Vouloir raisonner et calculer oblige donc à résoudre. Cependant, quand les règles de calcul s'appliquent, non seulement à des termes, mais aussi à des formules, résoudre des contraintes ne suffit plus et des opérations similaires doivent être utilisées à d'autres étapes de la recherche des démonstrations. Les algorithmes universels de résolution de contraintes, comme la surréduction, ont souvent été remplacés par des algorithmes spécialisés beaucoup plus efficaces. On s'interrogera dans cet exposé sur la possibilité d'opérer un remplacement similaire pour ces opérations.