Resolución Lógica:

En programación lógica se utiliza una única regla: la regla de resolución.

Utilizando esta regla y la demostración por reducción al absurdo podemos demostrar cualquier teorema dentro del subconjunto de lógica de predicados que tratamos (las cláusulas de Horn).

Vamos a ver la regla de resolución aplicada primero a lógica proposicional, y después la veremos ya aplicada a lógica de predicados.


Regla de resolución

Reglas habituales:

Ejemplo de refutación por resolución

Refutación de {{p, q}, {¬p, q}, {p, ¬q}, {¬p, ¬q}} :
      1 {p, q} Hipótesis
      2 {¬p, q} Hipótesis
      3 {p, ¬q} Hipótesis
      4 {¬p, ¬q} Hipótesis
      5 {q} Resolvente de 1 y 2
      6 {¬q} Resolvente de 3 y 4
      7 Resolvente de 5 y 6

Algoritmo de de resolución por saturación 

Def.: Sea S un conjunto de cláusulas.
         Res(S) = S ∪ ( S {Res(C1, C2) : C1, C2 ∈ S}).

Algoritmo de resolución por saturación

Entrada: Un conjunto finito de cláusulas, S.
Salida: Consistente, si S es consistente;
            Inconsistente, en caso contrario.

S 0 := ∅
mientras ( 6∈ S) y (S 6= S 0) hacer
       S 0 := S
       S := Res(S)
fmientras
si ( ∈ S) entonces
    Devolver Inconsistente
en caso contrario
    Devolver Consistente
fsi

Prop.: El algoritmo de resolución por saturación es correcto.

Programa para solucionar resolución:

Sin resultado de programas para la solucion de resoluciones logicas.


Bibliografia:

http://informatica.uv.es/iiguia/MD/prog_log3.pdf
https://www.cs.us.es/~jalonso/cursos/li-12/temas/tema-5.pdf