4.3.4 Resolucion General
La regla de Resolución General puede ser aplicada directamente a clausulas no atadas y hacer la unificacion como parate integral de la regla.
Deficinición 7.48 Sea
un conjunto de literales. Despues .Regla 7.49 (Regla de Resolución General) Sea
clausulas sin variables en común. Sea y subconjuntos de literales tales que y pueden ser unificadas por un mgu . y se dicen ser Clashing Clausulas y un clahs sobre el conjunto de literales y . C, la resolvente de , son la clausula:Ejemplo 7.50 Dadas 2 clausulas
yun mgu para
y es ,y la clausula resolvente a dar
La Regla de Resolución general requiere que las clausulas no tengan variables en común. Aqui todas las variables se renombran en una de las clausulas antes usadas en la regla de resolución. Recuerda que todas las variables en una clausula tienen implicito un cuantificador universal asi que la retitulacion no cambia la satisfiabilidad.
Ejemplo 7.51 para resolver 2 clausulas
y , primero se renombra las variables de la segunda clausula . Un mgu es , y y resuelve a ◘. las clausulas representan las formulas y , y y es obvio que la conjuncion es satisfacible.La regla de resolucion es definida como clausulas en un conjunto de literales, y la mgu
puede unificar al conjunto de literales clashing.ALGORITMO 7.53 (PROCEDIMIENTO DE RESOLUCION GENERAL)
Intrada:
conjunto de clasulas Salida: Las clausulas son satisfacibles o no satisfacibles. por lo tanto el algoritmo puede no terminar.Define
. Asume que se ha construido. Elija clausulas clashing y sea . Si ◘, termina el procedimiento: es no satisfacible. Si no, construye . Si para todos los posibles clashing de clausulas, termina el procedimiento: S es satisfacible.Mientras un conjunto de clausulas no satisfacible eventualmente producira ◘ debajo del sistema de ejecucion del procedimiento, la existecia de modelos infinitos significa que la ejecucion del procedimiento de resolucion sobre un conjunto de clausulas satisfacible puede nunca terminar.
Ejemplo 7.54 Lineas del 1 al 7 contiene un conjunto de clausulas no satifacibles. esta es mostrada en la linea 8 a la 15 las cuales dan una refutacion por el procedimiento de resolucion. Cada linea contiene la resolvente, la mgu y el numero de los pares de clausulas.
| 1. | |
| 2. | |
| 3. | |
| 4. | |
| 5. | |
| 6. | |
| 7. |
| 8. | 3,6 | ||
| 9. | 2,4 | ||
| 10. | 8,9 | ||
| 11. | 1,4 | ||
| 12. | 8,11 | ||
| 13. | 5,12 | ||
| 14. | 7,13 | ||
| 15. | ◘ | 10,14 |
| <= | Regresar Tema 4.3.3 Unificacion en Logica de Primer de Orden |
| => | Siguiente Tema: 4.4 Teorias y Demostracion de Teoremas |
| Regresar al TEMARIO: Matematicas Para Maestria |
