Rational Tarski Formula logically equivalent to the negation of expr

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.

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

$\mathrm{NegateFormula}\left(x=0\right)$

$x\ne 0$

$\mathrm{NegateFormula}\left(\mathrm{exists}\left(x\&comma;\mathrm{And}\left(x=0\&comma;y<0\right)\right)\right)$

$\forall \left(x\&comma;x\ne 0\vee 0\le y\right)$

$\mathrm{NegateFormula}\left(x=0⊻0<y\right)$

$\left(x\ne 0\wedge y\le 0\right)\vee \left(x=0\wedge 0<y\right)$

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

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