Impor

METODO DE RESOLUCION
“Todos los hombres son impacientes. Juan es un hombre. Consecuentemente, Juan es impaciente”.
Si asignamos a H(x) “x es un hombre”, a a (constante) “Juan” y aI(x) “x es impaciente”, entonces:
∀x [H(x) → I(x)], H(a) ∴ I(a).

Encontramos a continuación las formas normales de Skolem:
• FNS (∀x [H(x) → I(x)]) = ∀x [¬H(x) ∨ I(x)].
• FNS(H(a)) = H(a).
• FNS ( ¬I(a)) = ¬I(a).
A la hora de considerar las cláusulas, los cuantificadores no se tienen en cuenta, pero no hay que olvidar que todos son universales. Así pues, si enuna cláusula aparece una variable, esto quiere decir que estaba cuantificada y que el
cuantificador era universal.
El conjunto de cláusulas resultante es:
S = { ¬H(x) ∨ I(x), H(a),¬I(a) }.
con el conjunto de apoyo { ¬I(a) }.
El árbol de resolución correspondiente a este ejemplo sería el que presentamos a continuación:
Parece que no se puede continuar porqueen la cláusula troncal se tiene ¬I(a),
mientras que en la lateral se tiene I(x) y, dado que son diferentes, la regla de
resolución no se puede aplicar.
Efectivamente, la regla deresolución no se puede aplicar, ya que un literal no
es la negación del otro. Ahora bien, el literal I(x) contiene la variable x. Si esta
variable pudiese ser sustituida por la constantea, entonces la situación se desbloquearía. ¿Es posible esta sustitución?
La respuesta es afirmativa porque la cláusula troncal es realmente ∀x [¬H(x) ∨ I(x)]
y porque la regla deeliminación del cuantificador universal afirma que una variable cuantificada universalmente puede ser sustituida por cualquier término, y la
constante a es un término.
En conclusión, lavariable x se puede sustituir por la constante a (de hecho, lo
que se hace es aprovechar que ∀x [¬H(x) ∨ I(x)] ¬H(a) ∨ I(a)).
Así pues, obtendríamos el árbol de resolución siguiente: