¿Forma normal única de las fórmulas del cálculo de predicados?

Question

¿Existe una único forma normal para cada fórmula del cálculo de predicados?

Conozco las formas normales prenex del cálculo de predicados y las formas normales disyuntivas y conjuntivas del cálculo proposicional. Pero, ¿cómo se llama la combinación de ambas, es decir, la fórmula está en forma normal prenex y la matriz (sin cuantificador) está en -digamos- forma normal disyuntiva?

¿Puede lograrse siempre la unicidad mediante una elección óptima de las variables y la ordenación y disposición de los literales de la forma normal disyuntiva (dado que las variables y los símbolos de relación y función están ordenados lexicográficamente) y la eliminación de la doble negación?

Ejemplo : La forma normal única prevista de

$(\forall x_2) \neg R_2 (x_2) \rightarrow \Big((\exists x_1)\neg\neg R_3(x_1) \wedge R_1(x_1,x_2) \Big)$

debería ser (no estoy seguro)

$(\forall x_1)(\exists x_2)\big(R_1 (x_2,x_1) \vee R_2(x_1)\big) \wedge \big( R_2(x_1) \vee R_3 (x_2) \big)$

¿Cuál es la complejidad de encontrar tales formas normales?

Answer 1

Me gustaría señalar que el problema de la unicidad de una fórmula no es trivial incluso en la lógica proposicional. Por ejemplo, (p→q)∧(q→r)∧(r→p) es igual a (¬p∨q)∧(¬q∨r)∧(¬r∨p) y también a (¬p∨r)∧(¬r∨q)∧(¬q∨p).