Lógicas Clássicas
Procedimento para Obtenção da Forma Clausal
- Cláusula é uma disjunção de literais
1. Passar para a forma normal PRENEX.
2. Skolemizar as variáveis quantificadas existencialmente.
3. Abandona-se os quantificadores pré-fixados.
EXEMPLO
?x ?y ((? z (P(x,z) ^ P(y,z)) ? ? u Q(x,y,u)) =
- ?x ?y (? (? z (P(x,z) ^ P(y,z))) v ? u Q(x,y,u)) =
- ?x ?y (?z (? P(x,z) v ? P(y,z))) v ? u Q(x,y,u)) =
- ?x ?y ?z? u (? P(x,z) v ? P(y,z) v Q(x,y,u))
- ?x ?y ?z (? P(x,z) v ? P(y,z) v Q(x,y,f(x,y,z)))
- ? P(x,z) v ? P(y,z) v Q(x,y,f(x,y,z))
que é perfeitamente equivalente à fórmula original.