Lógicas Clássicas
Resolução
RESOLUÇÃO NA LÓGICA PROPOSICIONAL
EXEMPLO: P, (P ^ Q) ? R, S v T ? Q , T|? R
- Primeiro convertemos os axiomas em cláusulas.
1. P
2. ? P v ? Q v R
3. ? S v Q
4. ? T v Q
5. T
6. ? R
- Começamos então a escolher a par de cláusulas para resolver. Embora qualquer par de cláusulas possa ser resolvido, apenas aqueles pares que contenham literais complementares produzirão um resolvente com possibilidade de produzir uma cláusula vazia.