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).