Resolucion de predicados

¿Que es la resolución de predicados?

-Diseñada por J.A Robinson en 1965, significa que si un conjunto es insatisfactible, este algoritmo lo detecta y lo para. Si es satisfactible, podria detectarlo o no parar. EL algoritmo se basa en una inferencia sencilla

¿Cómo funciona?

-Resolución Proposicional:  Se cumple P o Q y la negacion P o R entonces se cumple Q o R.

Ejemplo: si se tiene un "Gana, empata o pierde" y "Si gana da una fiesta o va de viaje".  Se puede deducir que "O pierde o empata o da una fiesta o va de viaje".

Formalización:

P1: G v P v E
P2: G->F v V  es equivalente a ¬G v F v V

La regla de resolución inferirá: Dadas dos clausulas, C1 y C2 tales que exista un literal L de forma que L no pertenezca a C1 y ¬L  pertenezca a C2,  se denomina resolvente de C1 y C2 respecto a L.


Consistencia de la regla de resolución: el resolvente de los clausulas es consecuencia lógica de ellas. Es decir {C1,C2}=>R(C1,C2)

Resolución General:

Es una generalización de la resolución proposicional, el cual incluye un paso previo de unificación de clausulas mediante sustituciones.

Sustitución: 

Método para modificar formulas y su proposito para con la unificación en un conjunto de expresiones, y este resulten sintácticamente identicas.






Bibliografia:

http://di002.edv.uniovi.es/~labra/FTP/LPRED.pdf