Cierre de Congruencia

Un mecanismo algorítmico que calcula la relación de congruencia mínima que contiene un conjunto dado de igualdades sobre términos, típicamente fusionando clases de equivalencia y propagando congruencia de funciones para permitir un razonamiento eficiente sobre igualdades, especialmente en teorías de funciones no interpretadas.