Fermeture de Congruence

Un mécanisme algorithmique qui calcule la plus petite relation de congruence contenant un ensemble donné d'égalités entre termes, généralement en fusionnant des classes d'équivalence et en propageant la congruence des fonctions pour permettre un raisonnement égalitaire efficace, en particulier pour les fonctions non interprétées.