Resolución básica

De:
p <- q
q <- r
obtener:
p <- r

por manipulación lógica de las formas normales disyuntivas.

Solución:


Se formula la forma tradicional de implicación antecedente-consecuente para
las hipótesis:
q => p
r => q
Y se enuncia la respectiva fórmula para la conclusión:
r=>p
 Equivalentemente, se afirma que lo siguiente es una tautología:
 not [((not q) or p) and ((not r) or q)] or ((not r) or p)
Esto se puede comprobar por medio de una tabla de verdad, ver:
 https://www.wolframalpha.com/input/?i=not+%5B((not+q)+or+p)+and+((not+r)+or+q)%5D+or+((not+r)+or+p)
 (por ejemplo).
Aparentemente Lloyd toma el camino directo de sustitución, no el de
manipulación de formas normales (conjuntivas o disyuntivas); ver p. 40 y
41, donde se da la definición resolvente. Adoptaríamos ese camino; tal vez
después retornemos al de formas normales, pero por el momento no
es necesario. Ver en la p. 41 el concepto de refutation (por abundar de éste
en clase).