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
