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

Online Help

All Products    Maple    MapleSim


QuantifierElimination[QuantifierTools]

  

ConvertToPrenexForm

  

convert a (quantified) Tarski formula to prenex form

 

Calling Sequence

Parameters

Returns

Description

Examples

Compatibility

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 And or 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 Not operators, which are eliminated by negating the corresponding relations.

Examples

withQuantifierElimination:withQuantifierTools:

ConvertToPrenexFormAndNotx=0,existsy,xy=0

y,x0xy=0

(1)

ConvertToPrenexFormexistsy&comma;Andy&equals;0&comma;forallx&comma;0<1x

y&comma;x&comma;y=0x<0

(2)

Compatibility

• 

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

• 

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

See Also

AlphaConvert

QuantifierElimination

QuantifierTools