Considere as cláusulas C1 e C2, representadas, respectivamente, pelos conjuntos \(\{¬A(x),B(x)\}\) e \(\{A(g(y)),B(y)\}\). Um resolvente dessas cláusulas é

Gabarito

B

Comentário do professor

Temos \(C_1=\{\neg A(x),B(x)\}\) e \(C_2=\{A(g(y)),B(y)\}\). Para aplicar a regra da resolução buscamos literais complementares que se tornam idênticos por um unificador.

As literais complementares são \(\neg A(x)\) e \(A(g(y))\). O unificador mais geral é \(\theta=\{x\mapsto g(y)\}\). Aplicando \(\theta\) em ambas as cláusulas, \(\neg A(x)\) e \(A(g(y))\) tornam-se complementares idênticas e são eliminadas.

Os literais restantes, com \(\theta\) aplicada, são \(B(x)\theta = B(g(y))\) e \(B(y)\). A união desses literais forma o resolvente: \(\{B(g(y)),B(y)\}\).