NegateFormula - 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]

  

NegateFormula

  

negation of a rational Tarski formula

 

Calling Sequence

Parameters

Returns

Description

Examples

Compatibility

Calling Sequence

NegateFormula(expr)

Parameters

expr

-

Rational Tarski Formula

Returns

• 

Rational Tarski Formula logically equivalent to the negation of expr

Description

• 

NegateFormula does not just syntactically apply the 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 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

withQuantifierElimination:withQuantifierTools:

NegateFormulax=0

x0

(1)

NegateFormulaexistsx&comma;Andx&equals;0&comma;y<0

x&comma;x00y

(2)

NegateFormulaXorx&equals;0&comma;0<y

x0y0x=00<y

(3)

Compatibility

• 

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

• 

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

See Also

QuantifierElimination

QuantifierTools