cálculo de superposición

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 el manejo de igualdad basado en el ordenamiento, tal como se desarrolló en el contexto de la completitud de Knuth-Bendix (infalible) . Puede considerarse 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 demostrar la insatisfacibilidad de un conjunto de cláusulas de primer orden , es decir, realiza demostraciones por refutación . La superposición es completa en refutación : dados recursos ilimitados y una estrategia de derivación justa , de cualquier conjunto de cláusulas insatisfacibles se derivará eventualmente una contradicción.

Muchos demostradores de teoremas (de última generación) para la lógica de primer orden se basan en la superposición (por ejemplo, el demostrador de teoremas ecuacionales E ), aunque solo unos pocos implementan el cálculo puro.

• mi
• ESPAS
• Vampiro
• Waldmeister (página web oficial)

• Demostración de teoremas ecuacionales basada en reescritura con selección y simplificación , Leo Bachmair y Harald Ganzinger , Journal of Logic and Computation 3(4), 1994.
• Demostración de teoremas basada en paramodulación , Robert Nieuwenhuis y Alberto Rubio, Manual de razonamiento automatizado I(7), Elsevier Science y MIT Press , 2001.