En lógica proposicional , una inferencia de resolución es una instancia de la siguiente regla : [1]
Nosotros llamamos:
- Las cláusulas y son las premisas de la inferencia
- (el resolutivo de las premisas) es su conclusión.
- El literal es el literal resuelto por la izquierda,
- El literal es el literal correcto resuelto,
- es el átomo o pivote resuelto.
Esta regla se puede generalizar a la lógica de primer orden para: [2]
dónde es un unificador más general de y y y no tienen variables comunes.
Ejemplo
Las cláusulas y puede aplicar esta regla con como unificador.
Aquí x es una variable y b es una constante.
Aquí vemos que
- Las cláusulas y son las premisas de la inferencia
- (el resolutivo de las premisas) es su conclusión.
- El literal es el literal resuelto por la izquierda,
- El literal es el literal correcto resuelto,
- es el átomo o pivote resuelto.
- es el unificador más general de los literales resueltos.
Notas
- ^ Fontaine, Pascal; Merz, Stephan; Woltzenlogel Paleo, Bruno. Compresión de pruebas de resolución proposicional mediante regularización parcial . 23a Conferencia Internacional sobre Deducción Automatizada, 2011.
- ^ Enrique P. Arís, Juan L. González y Fernando M. Rubio, Lógica Computacional, Thomson, (2005).