El cálculo de superposición es un cálculo para el razonamiento en lógica ecuacional de primer orden . 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 terminación (infalible) de Knuth-Bendix . Puede verse como una generalización de la resolución (a la lógica ecuacional) o la 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 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.
A partir de 2007, la mayoría de los probadores de teoremas (de última generación) para la lógica de primer orden se basan en la superposición (por ejemplo, el demostrador del teorema de la ecuación E ), aunque solo unos pocos implementan el cálculo puro.
Implementaciones
- mi
- SPASS
- Vampiro
- Waldmeister (página web oficial)
Referencias
- Demostración del teorema de la ecuación basada en la reescritura con selección y simplificación , Leo Bachmair y Harald Ganzinger , Journal of Logic and Computation 3 (4), 1994.
- Demostración de teoremas basados en paramodulación , Robert Nieuwenhuis y Alberto Rubio, Handbook of Automated Reasoning I (7), Elsevier Science y MIT Press , 2001.