Resolução e Refutação na Lógica de Primeira Ordem

Resolução:

• 

• em que B e C são unificáveis sendo g a sua substituição unificadora mais geral.

A regra da resolução é correcta.

A regra da resolução não é completa.

Tal como na lógica proposicional, também aqui a refutação por resolução é completa.