Lógicas Clássicas
Resolução
RESOLUÇÃO NA LÓGICA DE PREDICADOS
- resolver apenas pares de cláusulas que contenham literias complementares, pois somente essas resoluções produzem clásulas novas mais difíceis de satisfazer que seus pais.
- Eliminar cláusulas do tipo tautologias e cláusulas que estejam incluídas em outras cláusulas (P v Q é incluída por P).
- Sempre que possível, resolver com uma das cláusulas que estamos tentando refutar ou com uma cláusula gerada por uma resolução com tal cláusula.
- Sempre que possível, dar preferência a cláusulas com um único literal.