The prenex equivalent of expr, that is, a string of quantified variables (the "prefix"), followed by a boolean formula of true/false values and/or polynomial constraints where the only allowable boolean operators are $\mathrm{And}$ or $\mathrm{Or}$.

Also alpha converts variables seen as conflicting in scope between quantified subformulae where appropriate, such that the output formula is correct and unambiguous as a quantified formula.

Uses equivalence of boolean operators, such as, e.g., Implies(A,B) = Or(Not(A),B).

Note the result does not contain any $\mathrm{Not}$ operators, which are eliminated by negating the corresponding relations.

$\mathrm{with}\left(\mathrm{QuantifierElimination}\right)\:$$\mathrm{with}\left(\mathrm{QuantifierTools}\right)\:$

$\mathrm{ConvertToPrenexForm}\left(\mathrm{And}\left(\mathrm{Not}\left(x=0\right)\,\mathrm{exists}\left(y\,xy=0\right)\right)\right)$

$\exists \left(y\,x\ne 0\wedge xy=0\right)$

$\mathrm{ConvertToPrenexForm}\left(\mathrm{exists}\left(y\&comma;\mathrm{And}\left(y=0\&comma;\mathrm{forall}\left(x\&comma;0<\frac{1}{x}\right)\right)\right)\right)$

$\exists \left(y\&comma;\forall \left(x\&comma;y=0\wedge -x<0\right)\right)$

The QuantifierElimination:-QuantifierTools:-ConvertToPrenexForm command was introduced in Maple 2023.

For more information on Maple 2023 changes, see Updates in Maple 2023.