Lógicas Clássicas
Resolução
EXEMPLO:
- Primeiro convertemos os axiomas em cláusulas.
1. Homem(Marco)
2. Pompeiano(Marco)
3. ? Pompeiano(x1) v Romano(x1)
4. Soberano(Cesar)
5. ? Romano(x2) v LealA(x2,Cesar) v Odiar(x2,Cesar)
6. LealA(x3,f1(x3)
7. ? Homem(x4) v ? Soberano(y1) v ? TentarAssassinar(x4,y1) v ? LealA(x4,y1)
8. TentarAssassinar(Marco,Cesar)
9. ? Odiar(Marco,Cesar)
- Começamos então a escolher o par de cláusulas para resolver.