Resolución: refutar la negación de una consulta

Queremos probar C desde KB = {A → (B ∨ C), A, ¬B}. Añadimos ¬C como hipótesis provisional. Si llegamos a la cláusula vacía □, entonces KB ⊨ C.

De fórmulas a cláusulas

A → (B ∨ C) ⇔ ¬A ∨ B ∨ C Hecho A Hecho ¬B Consulta C → añadir ¬C

Cláusulas disponibles

Forma un resolvente

Elige dos cláusulas y un átomo que aparezca en positivo en una y negado en la otra.

Qué acaba de pasar

  1. Cancela un par como A y ¬A. Copia los demás literales al resolvente.
  2. Si un resolvente contiene P y ¬P a la vez, es una tautología y no ayuda a cerrar la prueba.
  3. La cláusula vacía □ es falsa bajo cualquier asignación: señala contradicción.