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

Online Help

All Products    Maple    MapleSim


QuantifierElimination

  

DeleteFormula

  

incrementally produce the quantifier elimination result corresponding to deletion of a subformula from the input formula from a previous QE computation

 

Calling Sequence

Parameters

Description

Examples

Compatibility

Calling Sequence

DeleteFormula( data, atpos, relift = r, opts )

Parameters

data

-

QEData or CADData object from a previous QE computation

atpos

-

the atomic position of the subformula to delete from the prenex equivalent of the input formula from data - a positive integer, or a list of positive integers

r

-

(optional) truefalse; flag determining whether to relift the CAD tree where pure evolutionary CAD is used (default false)

opts

-

all keyword options applicable to poly-algorithmic QE (described in QuantifierElimination options)

Description

• 

"Evolutionary" method offering decrementality within QuantifierElimination.

• 

Performs QE on the input expression associated with data, but modified via arguments described above. Minimizes recomputation by using existing data from data.

• 

QEData and CADData objects can be obtained by requesting data via the output keyword option for all QuantifierElimination routines offering quantifier elimination. CADData is returned when the quantifier elimination was provided by PartialCylindricalAlgebraicDecompose.

• 

DeleteFormula is a routine offering generic decrementality including deletion of formulae at generic atomic positions for a previously used formula for quantifier elimination. This means that arbitrary subformulae can be deleted within a targeted subformula of a formula originally used for elimination. This means QE of similar formulae can better be explored without traversing the entire elimination process from scratch.

• 

The atomic position atpos provided must be a positive integer, or a list of such which describes the path through the unquantified part of the prenex formula previously used for elimination which is associated to data. The atomic position provided must be a viable atomic position for the formula to delete in light of the previously used formula.

• 

Atomic positions start their indexing from 1 and not 0.

• 

Relifting the CAD tree completely may be a performance detriment, but may be useful to prune the CAD tree such that it is of fewer cells.

Examples

withQuantifierElimination:withQuantifierTools:

exprforallx&comma;Implies0<x&comma;0<x2

exprx&comma;0<x0<x2

(1)

exprConvertToPrenexFormexpr

exprx&comma;0xx2<0

(2)

Perform QE on this formula. We will then investigate the variance of the first operand of the Or, i.e. varying the assumptions of the Implies in terms of the quantifier free equivalent of the entire formula.

qf&comma;w&comma;dataQuantifierEliminateexpr&comma;&apos;output&equals;qf&comma;witnesses&comma;data&apos;

qf,w,datatrue,,QEData forx&comma;x0x2<0

(3)

Produce the QE result corresponding to replacing x0 with x<0. In terms of the original formula with Implies, this will be equivalent to replacing 0<x with 0x. We will do this in two steps - with a deletion then an insertion to achieve the replacement.

qf&comma;w&comma;dataDeleteFormuladata&comma;1&comma;&apos;output&equals;qf&comma;witnesses&comma;data&apos;

qf,w,datafalse,false&comma;x=0,QEData forx&comma;x2<0

(4)

Reinstate the disjunction lost as part of the last call but with x<0. Do this via an insertion.

q&comma;w&comma;dataInsertFormuladata&comma;&apos;Or&apos;&comma;1&comma;x<0&comma;&apos;output&equals;qf&comma;witnesses&comma;data&apos;

q,w,datafalse,false&comma;x=0,QEData forx&comma;x<0x2<0

(5)

Overall we see the formula is now false due to the edge case introduced by x=0, which is included as part of the new assumption replacing the old 0<x.

Compatibility

• 

The QuantifierElimination:-DeleteFormula command was introduced in Maple 2023.

• 

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

See Also

InsertFormula

PartialCylindricalAlgebraicDecompose

QuantifierEliminate

QuantifierElimination