## [Cierre de Congruencia](/es/node/60856) Definición 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. ## Principio Principio Mantener clases de equivalencia de términos bajo igualdades afirmadas, fusionar clases cuando aparezcan igualdades y asegurar que si f(a1,...,an) y f(b1,...,bn) están presentes y ai ≡ bi para todo i, entonces los términos compuestos también se fusionen, repitiendo hasta alcanzar el cierre. ## Demostración Demostración Dadas las igualdades a = b y f(a) = c, el cierre fusiona a y b en una clase, reconoce que f(a) y f(b) son equivalentes y fusiona sus clases, lo que permite al solucionador deducir ulteriormente igualdades o contradicciones de manera eficiente. ## Aplicación incorrecta Aplicación incorrecta Aplicar el cierre de congruencia de forma ingenua en grafos de términos muy grandes sin hash-consing o union-by-rank puede provocar un gran aumento de coste y memoria; el manejo incorrecto de aridades de símbolos de función o de tipos puede producir fusiones no válidas. ## Consecuencia Consecuencia Un cierre de congruencia correcto proporciona razonamiento de igualdades rápido y canónico usado en motores SMT y demostradores, permitiendo verificaciones de representantes en tiempo constante y actualizaciones incrementales a medida que se añaden igualdades. ## Inversión Inversión La inversión es tratar las igualdades solo por emparejamiento sintáctico sin propagación de cierre: esto conserva las igualdades iniciales pero omite muchas igualdades implícitas y ofrece menor potencia de razonamiento. ## Límite Límite Se dirige al razonamiento de igualdad para funciones no interpretadas en términos de primer orden y igualdades ground; no maneja por sí solo teorías interpretadas (aritmética, arreglos) sin combinarse con otros solucionadores de teoría. ## Tensión semántica Tensión semántica Existe tensión entre el cierre de congruencia y el tratamiento de igualdades estilo resolución: el cierre de congruencia proporciona mantenimiento incremental impulsado por estructuras de datos, mientras la resolución maneja igualdades mediante manipulación e inferencia de cláusulas. ## Síntesis Síntesis El cierre de congruencia fusiona incrementalmente clases de equivalencia de términos y propaga la congruencia de funciones para formar la congruencia mínima que contiene las igualdades dadas, ofreciendo razonamiento de igualdad compacto y eficiente que se integra naturalmente en procedimientos SMT y de decisión.