El cálculo de superposición es un cálculo para el razonamiento 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 pedidos, tal como se desarrolló en el contexto de la finalización (infalible) de Knuth-Bendix . Puede verse como una generalización de resolución (a la lógica ecuacional) o de finalización infalible (a la lógica clausal completa ). Como la mayoría de los cálculos de primer orden , la superposición intenta mostrar la insatisfacción de un conjunto de cláusulas de primer orden , es decir, realiza pruebas por refutación . La superposición es una refutación completa : dados recursos ilimitados y una estrategia de derivación justa , de cualquier conjunto de cláusulas insatisfactorias eventualmente se derivará una contradicción.
Muchos demostradores de teoremas (de última generación) para la lógica de primer orden se basan en la superposición (p. ej., el demostrador del teorema ecuacional E ), aunque sólo unos pocos implementan el cálculo puro.