Lógicas Clássicas
Resolução
RESOLUÇÃO NA LÓGICA DE PREDICADOS
1. Converter todas as declarações de F em cláusulas.
2. Negar S e converter o resultado em cláusulas. Acrescentá-las ao conjunto de cláusulas obtidas em 1.
3. Repetir até que uma contradição seja encontrada, e nenhum progresso possa ser feito, ou até que se tenha gasto um quantidade pré-determinada de esforço:
3.1. Escolher duas cláusulas e chamá-las de cláusulas pais.
3.2. Resolvê-las. O resolvente será a disjunção de todos os literais de ambas as cláusulas pais com as substituições apropriadas realizadas, ressalvando-se o seguinte:
3.2.1. Se houver um par de literais T1 e ? T2 tal que uma das cláusulas pais contenha T1 e a outra contenha T2, e ainda se T1 e T2 forem unificáveis, então nem T1 nem T2 devem aparecer no resolvente.
3.2.2. Chamaremos T1 e T2 literais complementares. Utilize a substituição produzida pela unificação para criar o resolvente.