Forma normal clausal: diferenças entre revisões

 

#Coloque a fórmula na [[Forma normal prenex|forma normal prenex]];

#[[Skolemização|Skolemize]] - substitua as variáveis existenciais por constantes de [[Thoralf Skolem|Skolem]] ou funções de Skolem de variáveis universais, de fora para dentro. Faça as seguintes substituições:

#* <math>\exists x. P(x)</math> torna-se <math>P(c)</math>, onde <math>c</math> é novo.