Skolemização: diferenças entre revisões

 

:::::::::<math>\forall x_2 .\forall x_4 .\forall x_3 .\lnot (P(f(x_2),x_2) \rightarrow \lnot (P(x_3,x_4) \land R(a)))</math>

 

Note que no processo de skolemização a variável <math>\qquad x_1</math> foi substituída pelo termo de função <math>\qquad f(x_2)</math> e não por <math>\qquad f(x_2, x_4)</math>, pois <math>\qquad x_4</math> não faz parte da mesma fórmula atômica de <math>\qquad x_1</math>.