El cálculo de superposición es un cálculo para razonar en lógica ecuacional . Fue desarrollado a principios de la década de 1990 y combina conceptos de resolución de primer orden con manejo de igualdad basado en ordenamiento como se desarrolló en el contexto de la completitud (infalible) de Knuth-Bendix . Puede verse como una generalización de la resolución (a la lógica ecuacional) o de la completitud infalible (a la lógica clausal completa ). Como la mayoría de los cálculos de primer orden , la superposición intenta mostrar la insatisfacibilidad de un conjunto de cláusulas de primer orden , es decir, realiza pruebas por refutación . La superposición es refutación completa : dados recursos ilimitados y una estrategia de derivación justa , de cualquier conjunto de cláusulas insatisfacibles eventualmente se derivará una contradicción.
Muchos demostradores de teoremas (de última generación) para lógica de primer orden se basan en la superposición (por ejemplo, el demostrador de teoremas de ecuaciones E ), aunque sólo unos pocos implementan el cálculo puro.