RESOLUCION DE PREDICADOS

INTRODUCCION

Creado por J.A Robinson en 1965 lo que plante es que el algoritmo cuando detecta un conjunto de cláusulas es insatisfactible se detiene. Si es satisfactible podría detectarlo o no detenerse, y por lo tanto queda incompleto en funcionamiento. Según Robinson, demostró con su regla de resolución que...” sólo con ella y con un algoritmo de refutación y búsqueda en extensión resulta un sistema deductivo consistente y completo para la lógica de predicados".

La resolución es una técnica utilizada para resolver teoremas en lógica y utiliza la refutación para determinar una sentencia determinada.

Ésta se basa en negar la sentencia original para intentar crear una contradicción, demostrando de esta manera que la sentencia original es verdadera. Se aplica a sentencias escritas en forma clausulada. Básicamente, se busca demostrar que la negación de una sentencia genera una contradicción con los hechos conocidos, es decir, que no es satisfacible.

Pasos para lograr la resolución:

1.    Se convierten todas las cláusulas a la forma clausal. 

2.    Se niega el estatuto a probar, se convierte a forma clausal, y se agrega a las cláusulas del punto  (1). 

3.    Se repite lo siguiente hasta encontrar una contradicción. Se escogen dos cláusulas que se    llamarán cláusulas padre, luego, se busca en ellas un par de literales TI y ¬TI tal que una de ellas pertenezca a una cláusula padre y su negación a la otra cláusula padre. Se eliminan ambas literales y se crea el resolvente (se usa la unificación). La cláusula resultante se llama cláusula resolvente y si ésta es vacía, la contradicción fue encontrada; si no, la cláusula resolvente se agrega al conjunto de las demás.

Ejemplo:

                A. Jack es dueño de un perro

                B. Quien es dueño de un perro es amante de los animales

                C. Ningún amante de los animales mata a un animal

                D. O Jack o Curiosidad mató al gato, cuyo nombre era Tuna

                E. ¿Mató Curiosidad al gato?

Pasos:

           Expresar lo anterior como predicados de primer orden, por ejemplo:

            Jack es dueño de un perro: (Ǝ X) perro(X) ^ dueño(Jack, X).

2.                          Se niega el estatuto a probar:

            E. ¬ mata (curiosidad, tuna)

3.                          Se siguen los 8 pasos para transformar las sentencias a su forma

           Clausulada con lo que se obtiene el siguiente conjunto de cláusulas:

           A1. perro(a)

           A2. dueño(jack, a)

             B. ¬ perro(Z) ˅ ¬ dueño(Y, Z) ˅ naturalista(Y)

             C. ¬ naturalista(U) ˅ ¬ animal(W) ˅ ¬ mata(U,W)

           D1. mata(Jack, tuna) ˅ mata(curiosidad, tuna)

           D2. gato(tuna)

             E. ¬ mata(curiosidad, tuna)

             F. ¬ gato(C) ˅ animal

BIBLIOGRAFIA

http://www.kramirez.net/Robotica/Investigacion/II2015/LogicaPrimerOrden/Presentaci%C3%B3n%20de%20la%20investigaci%C3%B3n.pdf