ConvertToPrenexForm - Maple Help
For the best experience, we recommend viewing online help using Google Chrome or Microsoft Edge.

QuantifierElimination[QuantifierTools]

 ConvertToPrenexForm
 convert a (quantified) Tarski formula to prenex form

 Calling Sequence ConvertToPrenexForm( expr )

Parameters

 expr - Rational Tarski formula, usually quantified

Returns

 • 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}$.

Description

 • 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.

Examples

 > $\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 }{x}{}{y}{=}{0}\right)$ (1)
 > $\mathrm{ConvertToPrenexForm}\left(\mathrm{exists}\left(y,\mathrm{And}\left(y=0,\mathrm{forall}\left(x,0<\frac{1}{x}\right)\right)\right)\right)$
 ${\exists }{}\left({y}{,}{\forall }{}\left({x}{,}{y}{=}{0}{\wedge }{-}{x}{<}{0}\right)\right)$ (2)

Compatibility

 • The QuantifierElimination:-QuantifierTools:-ConvertToPrenexForm command was introduced in Maple 2023.
 • For more information on Maple 2023 changes, see Updates in Maple 2023.