Como se constrói um resolvente entre duas cláusulas na resolução de primeira-ordem?

Resposta

Aplicando o MGU aos literais complementares e unindo os literais restantes após a substituição.

Explicação:
1. Identificar literais complementares \(L\) e \(\neg L'\).
2. Encontrar o unificador mais geral \(\theta\) tal que \(L\theta = L'\theta\).
3. Aplicar \(\theta\) em ambas as cláusulas, remover as literais unificadas e unir os literais restantes para obter o resolvente.

Exemplo:
Considere \(C_1=\{\neg P(f(x)),Q(x)\}\) e \(C_2=\{P(z),R(z)\}\).
Literais complementares: \(\neg P(f(x))\) e \(P(z)\).
MGU: \(\theta=\{z\mapsto f(x)\}\).
Aplicando \(\theta\): \(Q(x)\theta=Q(x)\) e \(R(z)\theta=R(f(x))\).
Resolvente: \(\{Q(x),R(f(x))\}\).