Lógicas Clássicas
Resolução
RESOLUÇÃO NA LÓGICA PROPOSICIONAL
3. Repetir até que seja encontrada uma contradição ou não se possa fazer progresso:
3.1. Escolher duas cláusulas, que serão chamadas cláusulas pais.
3.2. Resolva-as. A cláusula resultante, denominada resolvente, será a disjunção de todos os literais de ambas as cláusulas pais, com a seguinte exceção:
Se houver qualquer par de literais L e ? L, tal que uma das cláusulas pais contenha L e a outra ? L, então elimine tanto L como ? L do resolvente.
3.3. Se o resolvente for uma cláusula vazia, terá sido encontrada uma contradição. Se não for, acrescente-o ao conjunto de cláusulas disponíveis para o procedimento.