NegateFormula - Maple Help

QuantifierElimination[QuantifierTools]

 NegateFormula
 negation of a rational Tarski formula

 Calling Sequence NegateFormula(expr)

Parameters

 expr -

Returns

 • Rational Tarski Formula logically equivalent to the negation of expr

Description

 • NegateFormula does not just syntactically apply the $\mathrm{Not}$ operator, but instead processes the expr recursively to push the negation to the innermost relations, i.e., if expr does not itself contain any $\mathrm{Not}$ operators, then neither does the result.
 • The output will only be in prenex form if the input was - i.e. if the input features quantified expressions as arguments to boolean operators then the output will have the same property.
 • In other words, the logical structure is (mostly) retained, but perhaps with different operators.

Examples

 > $\mathrm{with}\left(\mathrm{QuantifierElimination}\right):$$\mathrm{with}\left(\mathrm{QuantifierTools}\right):$
 > $\mathrm{NegateFormula}\left(x=0\right)$
 ${x}{\ne }{0}$ (1)
 > $\mathrm{NegateFormula}\left(\mathrm{exists}\left(x,\mathrm{And}\left(x=0,y<0\right)\right)\right)$
 ${\forall }{}\left({x}{,}{x}{\ne }{0}{\vee }{0}{\le }{y}\right)$ (2)
 > $\mathrm{NegateFormula}\left(\mathrm{Xor}\left(x=0,0
 $\left({x}{\ne }{0}{\wedge }{y}{\le }{0}\right){\vee }\left({x}{=}{0}{\wedge }{0}{<}{y}\right)$ (3)

Compatibility

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