Resolucion Atada

4.3.1 Resolucion Atada.

Ahora ampliaremos el Método de Resolución para el cálculo de predicados. Este será hecho en dos etapas: primero, defineremos una simple, pero ineficiente, versión llamada Resolución Atada, y entonces se define Substitución y Unificación, los cuales son usados en el Método de Resolución General.

Método 7.28(Método de Resolución Atada)

son cláusulas atadas tal que l y l^c . , la resolvente de y , es la cláusula:

            Res(
)=(
-
(
{lc
).

La resolvente de C es satisfacible si y solo si las cláusulas

y son mutuamente satisfacibles.

y son cláusulas satisfacibles las cuales son embonadas en la literal l, l^c. Por el teorema 7.22, Estas son satisfacibles en la interpretación de Herbrand H. Tenemos que B es un subconjunto de Herbrand que define a H como,

              
|VH(P(
,…,
))=T 

Esto es para terminos atados de

. Dos literales atadas complementarias no pueden ser elementos de B. Esto es is l B, para es satisfacible en H tendría otra literal l’ la cual l’ B. Para la construcción de la resolvente C usando las reglas de resolución , l’ C, y V_H©=T, esto es, H es modelo para C.

El procedimiento de resolución atada es definido como el procedimiento de resolución para el cálculo proposicional. Dado un conjunto de cláusulas atadas, los pasos de resolución son cambiados repetitivamente. El conjunto de clásulas atadas son insatisfacibles si en alguno de los pasos de la resolución se produce una cláusula vacía.

<=	Regresar Tema 4.3 Resolucion en Logica de Primer Orden

=>	Siguiente Tema: 4.3.2 Sustitucion en Logica de Primer Orden

Regresar al TEMARIO: Matematicas Para Maestria