Lógicas Clássicas
Resolução
RESOLUÇÃO NA LÓGICA DE PREDICADOS
3.3. Se o resolvente for uma cláusula vazia, então foi encontrada uma contradição. Se não for, acrescente-o ao conjunto de cláusulas disponíveis para o procedimento.
- Se a escolha de cláusulas a resolver em cada passo for feita de maneira sistemática, o procedimento de resolução encontrará uma contradição, se ela existir.
- Isto contudo, poderá levar muito tempo.
- Existem estratégias opcionais para acelerar o processo.