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

Online Help

All Products    Maple    MapleSim

QuantifierElimination

 InsertFormula
 incrementally produce the QE result corresponding to insertion of a Tarski formula into the input formula from a previous QE computation

 Calling Sequence InsertFormula( data, operation, atpos, newformula, relift = r, opts )

Parameters

 data - QEData or CADData object from a previous QE computation operation - operation with which to insert the new formula with - either And or Or atpos - the atomic position of the formula from data at which to insert the new formula - a positive integer, or a list of positive integers newformula - new formula to be inserted at atomic position atpos via operation r - (optional) truefalse; flag determining whether to relift the CAD tree where pure evolutionary CAD is used (default $\mathrm{false}$) opts - all keyword options applicable to poly-algorithmic QE (described in QuantifierElimination options)

Description

 • "Evolutionary" method offering incrementality within QuantifierElimination.
 • Performs QE on the input expression associated with data, but modified via the parameters described above. Minimizes recomputation by using existing data structures 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.
 • InsertFormula is a routine offering generic incrementality including insertion of formulae at generic atomic positions. This means that arbitrary formulae can be added within a targeted subformula of a formula originally used for elimination.
 • 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 inserting formula in light of the previously used formula. This means QE of similar formulae can better be explored without traversing the entire elimination process from scratch.
 • Atomic positions start their indexing from 1 and not 0.
 • If using InsertFormula starting from CADData, then if newformula introduces new free variables to the formula, the CAD will be relifted regardless of the value of r, which may be slow. One should begin with a core formula that covers all free variables, if possible.

Examples

 > $\mathrm{with}\left(\mathrm{QuantifierElimination}\right):$$\mathrm{with}\left(\mathrm{QuantifierTools}\right):$
 > $\mathrm{expr}≔\mathrm{forall}\left(x,0
 ${\mathrm{expr}}{≔}{\forall }{}\left({x}{,}{0}{<}{x}{⇒}{0}{<}{{x}}^{{2}}\right)$ (1)
 > $\mathrm{expr}≔\mathrm{ConvertToPrenexForm}\left(\mathrm{expr}\right)$
 ${\mathrm{expr}}{≔}{\forall }{}\left({x}{,}{0}{\le }{-}{x}{\vee }{-}{{x}}^{{2}}{<}{0}\right)$ (2)

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

 > $\mathrm{qf},w,\mathrm{data}≔\mathrm{QuantifierEliminate}\left(\mathrm{expr},'\mathrm{output}=\left[\mathrm{qf},\mathrm{witnesses},\mathrm{data}\right]'\right)$
 ${\mathrm{qf}}{,}{w}{,}{\mathrm{data}}{≔}{\mathrm{true}}{,}\left[\right]{,}{\mathrm{QEData for}}{}{\forall }{}\left({x}{,}{x}{\le }{0}{\vee }{-}{{x}}^{{2}}{<}{0}\right)$ (3)

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

 > $\mathrm{qf},w,\mathrm{data}≔\mathrm{DeleteFormula}\left(\mathrm{data},1,'\mathrm{output}=\left[\mathrm{qf},\mathrm{witnesses},\mathrm{data}\right]'\right)$
 ${\mathrm{qf}}{,}{w}{,}{\mathrm{data}}{≔}{\mathrm{false}}{,}\left[\left[{\mathrm{false}}{,}{x}{=}{0}\right]\right]{,}{\mathrm{QEData for}}{}{\forall }{}\left({x}{,}{-}{{x}}^{{2}}{<}{0}\right)$ (4)

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

 > $q,w,\mathrm{data}≔\mathrm{InsertFormula}\left(\mathrm{data},'\mathrm{Or}',1,x<0,'\mathrm{output}=\left[\mathrm{qf},\mathrm{witnesses},\mathrm{data}\right]'\right)$
 ${q}{,}{w}{,}{\mathrm{data}}{≔}{\mathrm{false}}{,}\left[\left[{\mathrm{false}}{,}{x}{=}{0}\right]\right]{,}{\mathrm{QEData for}}{}{\forall }{}\left({x}{,}{x}{<}{0}{\vee }{-}{{x}}^{{2}}{<}{0}\right)$ (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.

Compatibility

 • The QuantifierElimination:-InsertFormula command was introduced in Maple 2023.
 • For more information on Maple 2023 changes, see Updates in Maple 2023.

 See Also