Lógicas Clássicas
Procedimento para Obtenção da Forma Normal Prenex
1. Eliminar os conectivos lógicos ? e ? usando as seguintes leis:
- F ? G = (F ? G) ^ (G ? F)
- (F ? G) = ? F v G
2. Repetir o uso das seguintes leis:
- ? ? F = F
- ? (F v G) = ? F ^ ? G
- ? (F ^ G) = ? F v ? G
- ? (?xF(x)) = ? x(? F(x))
- ? (? x F(x)) = ?x(? F(x)
Estas leis são utilizadas para trazer os sinais de negação para antes dos átomos.
3. Padronizar as variáveis, se necessário, de modo que cada quantificador possua sua própria variável.