Un procedimiento algorítmico que, dada una colección de igualdades entre términos ground (o términos en una signatura), calcula la relación de congruencia mínima que contiene esas igualdades —es decir, la menor relación de equivalencia cerrada bajo la aplicación de símbolos de función— para decidir el entailment ecuacional.

Principio

Cerrar las igualdades de entrada bajo reflexividad, simetría, transitividad y congruencia: si a=b entonces para cualquier contexto f(...,a,...) y f(...,b,...) los resultados son equivalentes; en implementación esto se realiza mediante union‑find sobre representantes de términos más propagación de congruencia hasta alcanzar un punto fijo.

Demostración

Con ecuaciones a=b y b=c y una función binaria f, el algoritmo unirá a,b,c y añadirá que f(a,d) es equivalente a f(c,d) para cualquier término d, repitiendo hasta que no emerjan nuevas congruencias; variantes prácticas construyen y fusionan clases de congruencia incrementalmente para manejar firmas grandes de forma eficiente.

Aplicación incorrecta

Usar un algoritmo de cierre de congruencia para términos ground sin adaptar ante variables libres o teorías interpretadas produce resultados no válidos o incompletos; igualmente, tratar el cierre de congruencia como sustituto de la prueba completa en teorías combinadas puede omitir inferencias específicas de la teoría.

Consecuencia

Proporciona un procedimiento de decisión para el entailment ecuacional ground en la teoría de funciones no interpretadas, usado ampliamente como motor en SMT y sistemas de razonamiento automático; las implementaciones eficientes alcanzan tiempos cercanos al lineal en entradas típicas.

Inversión

En lugar de calcular la menor congruencia que contiene las igualdades, se puede calcular una relación sobredimensionada (por ejemplo una aproximación basada en tipos) o subconjuntos de igualdades; estas inversiones sacrifican corrección o completitud por rapidez o sencillez.

Límite

El cierre de congruencia estándar se aplica principalmente a términos ground y símbolos de función no interpretados; su extensión a fórmulas cuantificadas, teorías interpretadas (p. ej. aritmética) o igualdades condicionales requiere maquinaria adicional como instanciación de cuantificadores, solucionadores de teoría o procedimientos de completación.

Tensión semántica

Suele confundirse con unificación o con procedimientos de completación por reescritura: la unificación halla sustituciones que hacen términos iguales, la completación produce sistemas de reescritura confluyentes, mientras que el cierre de congruencia calcula clases de equivalencia de términos ground —relacionadas pero operacionalmente distintas tareas.

Síntesis

El algoritmo de cierre de congruencia construye la mínima relación de equivalencia sobre términos cerrada bajo aplicación de funciones mediante el fusión iterativa de clases y la propagación de congruencias; es el núcleo práctico para decidir consecuencias ecuacionales ground en muchos marcos de razonamiento automático.