 RegularChains[SemiAlgebraicSetTools] - Maple Programming Help

Home : Support : Online Help : Mathematics : Factorization and Solving Equations : RegularChains : SemiAlgebraicSetTools Subpackage : RegularChains/SemiAlgebraicSetTools/QuantifierElimination

RegularChains[SemiAlgebraicSetTools]

 QuantifierElimination
 returns an equivalent formula free of quantifiers

 Calling Sequence QuantifierElimination(f, R, opts)

Parameters

 f - a quantified logic formula R - (optional) polynomial ring opts - (optional) one or more options of the form output = rootof (literally) or simplification = simpval (where simpval is one of: false, L1, L2, L3, L4)

Description

 • The command QuantifierElimination(f) returns a quantifier-free logic formula  $\mathrm{qff}$ logically equivalent to f.
 • The user interface of Quantifier Elimination relies on the features of the Logic package. In addition to those features, we denote by &E the existential quantifier $\exists$ and by &A the universal quantifier $\forall$.
 • Extended Tarski formulas are supported with the option output=rootof.
 • The output formulas can be simplified using different levels of heuristical optimizations, from the lower-level simplification = L1 to the higher-level simplification = L4.

Examples

 > $\mathrm{with}\left(\mathrm{RegularChains}\right):$
 > $\mathrm{with}\left(\mathrm{SemiAlgebraicSetTools}\right):$

Suppose that we would like to solve the following Quantifier Elimination (QE) problem (due to Davenport and Heintz): find a logic formula involving $d$ only and which is logically equivalent to the following formula

$\mathrm{\exists }c\phantom{\rule[-0.0ex]{1.5ex}{0.0ex}}\mathrm{\forall }\left(b,a\right)\phantom{\rule[-0.0ex]{1.5ex}{0.0ex}}\left(\left(\left(a=d\wedge b=c\right)\vee \left(a=c\wedge b=1\right)\right)\mathbf{⇒}{a}^{2}=b\right)\phantom{\rule[-0.0ex]{0.5ex}{0.0ex}}$

We first define a logic formula:

 > $f≔&E\left(\left[c\right]\right),&A\left(\left[b,a\right]\right),\left(\left(\left(a=d\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&and\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(b=c\right)\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&or\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(\left(a=c\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&and\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(b=1\right)\right)\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&implies\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({a}^{2}=b\right)$
 ${f}{≔}{&E}{}\left(\left[{c}\right]\right){,}{&A}{}\left(\left[{b}{,}{a}\right]\right){,}\left(\left(\left({a}{=}{d}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{&and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({b}{=}{c}\right)\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{&or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(\left({a}{=}{c}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{&and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({b}{=}{1}\right)\right)\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{&implies}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({{a}}^{{2}}{=}{b}\right)$ (1)

Then we invoke the QuantifierElimination command on the above formula

 > $\mathrm{out}≔\mathrm{QuantifierElimination}\left(f\right)$
 ${\mathrm{out}}{≔}\left({d}{-}{1}{=}{0}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{&or}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({d}{+}{1}{=}{0}\right)$ (2)

Note that in the previous example, no variable order is specified.  In such case, the QuantifierElimination command will try to find the best elimination order according to some heuristical strategy. Alternatively, one can specify a variable order by using the PolynomialRing command as follows.

 > $R≔\mathrm{PolynomialRing}\left(\left[x,a,b,c\right]\right)$
 ${R}{≔}{\mathrm{polynomial_ring}}$ (3)

On this second example below, the command QuantifierElimination(f, R) computes necessary and sufficient conditions on a, b, c for the equation to have solutions in x.

 > $f≔&E\left(\left[x\right]\right),a{x}^{2}+bx+c=0$
 ${f}{≔}{&E}{}\left(\left[{x}\right]\right){,}{a}{}{{x}}^{{2}}{+}{b}{}{x}{+}{c}{=}{0}$ (4)
 > $\mathrm{out}≔\mathrm{QuantifierElimination}\left(f,R\right)$
 ${\mathrm{out}}{≔}{\mathrm{&or}}{}\left({c}{=}{0}{,}{\mathrm{&and}}{}\left({c}{<}{0}{,}{b}{<}{0}{,}{a}{=}{0}\right){,}{\mathrm{&and}}{}\left({c}{<}{0}{,}{b}{<}{0}{,}{0}{<}{a}\right){,}{\mathrm{&and}}{}\left({c}{<}{0}{,}{b}{<}{0}{,}{4}{}{a}{}{c}{-}{{b}}^{{2}}{=}{0}\right){,}{\mathrm{&and}}{}\left({c}{<}{0}{,}{b}{<}{0}{,}{a}{<}{0}{,}{4}{}{a}{}{c}{-}{{b}}^{{2}}{<}{0}\right){,}{\mathrm{&and}}{}\left({c}{<}{0}{,}{b}{=}{0}{,}{0}{<}{a}\right){,}{\mathrm{&and}}{}\left({c}{<}{0}{,}{0}{<}{b}{,}{a}{=}{0}\right){,}{\mathrm{&and}}{}\left({c}{<}{0}{,}{0}{<}{b}{,}{0}{<}{a}\right){,}{\mathrm{&and}}{}\left({c}{<}{0}{,}{0}{<}{b}{,}{4}{}{a}{}{c}{-}{{b}}^{{2}}{=}{0}\right){,}{\mathrm{&and}}{}\left({c}{<}{0}{,}{0}{<}{b}{,}{a}{<}{0}{,}{4}{}{a}{}{c}{-}{{b}}^{{2}}{<}{0}\right){,}{\mathrm{&and}}{}\left({0}{<}{c}{,}{b}{<}{0}{,}{a}{<}{0}\right){,}{\mathrm{&and}}{}\left({0}{<}{c}{,}{b}{<}{0}{,}{a}{=}{0}\right){,}{\mathrm{&and}}{}\left({0}{<}{c}{,}{b}{<}{0}{,}{4}{}{a}{}{c}{-}{{b}}^{{2}}{=}{0}\right){,}{\mathrm{&and}}{}\left({0}{<}{c}{,}{b}{<}{0}{,}{0}{<}{a}{,}{4}{}{a}{}{c}{-}{{b}}^{{2}}{<}{0}\right){,}{\mathrm{&and}}{}\left({0}{<}{c}{,}{b}{=}{0}{,}{a}{<}{0}\right){,}{\mathrm{&and}}{}\left({0}{<}{c}{,}{0}{<}{b}{,}{a}{<}{0}\right){,}{\mathrm{&and}}{}\left({0}{<}{c}{,}{0}{<}{b}{,}{a}{=}{0}\right){,}{\mathrm{&and}}{}\left({0}{<}{c}{,}{0}{<}{b}{,}{4}{}{a}{}{c}{-}{{b}}^{{2}}{=}{0}\right){,}{\mathrm{&and}}{}\left({0}{<}{c}{,}{0}{<}{b}{,}{0}{<}{a}{,}{4}{}{a}{}{c}{-}{{b}}^{{2}}{<}{0}\right)\right)$ (5)

By default, QuantifierElimination returns the standard quantifier-free formula, namely the Tarski formula. Extended Tarski formulas are supported by the option output=rootof.

 > $f≔&E\left(\left[x\right]\right),a{x}^{2}+bx+c=0$
 ${f}{≔}{&E}{}\left(\left[{x}\right]\right){,}{{x}}^{{2}}{}{a}{+}{x}{}{b}{+}{c}{=}{0}$ (6)
 > $\mathrm{out}≔\mathrm{QuantifierElimination}\left(f,'\mathrm{output}'='\mathrm{rootof}'\right)$
 ${\mathrm{out}}{≔}{\mathrm{&or}}{}\left(\left({a}{<}{0}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{&and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(\frac{{{b}}^{{2}}}{{4}{}{a}}{\le }{c}\right){,}\left({a}{=}{0}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{&and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({b}{\ne }{0}\right){,}{\mathrm{&and}}{}\left({a}{=}{0}{,}{b}{=}{0}{,}{c}{=}{0}\right){,}\left({0}{<}{a}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{&and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({c}{\le }\frac{{{b}}^{{2}}}{{4}{}{a}}\right)\right)$ (7)
 > $f≔&E\left(\left[y\right]\right),{y}^{2}+{x}^{2}=2$
 ${f}{≔}{&E}{}\left(\left[{y}\right]\right){,}{{x}}^{{2}}{+}{{y}}^{{2}}{=}{2}$ (8)
 > $\mathrm{out}≔\mathrm{QuantifierElimination}\left(f,\mathrm{output}=\mathrm{rootof}\right)$
 ${\mathrm{out}}{≔}\left({-}\sqrt{{2}}{\le }{x}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{&and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({x}{\le }\sqrt{{2}}\right)$ (9)
 > $f≔&E\left(\left[y\right]\right),{y}^{4}+{x}^{4}=2$
 ${f}{≔}{&E}{}\left(\left[{y}\right]\right){,}{{x}}^{{4}}{+}{{y}}^{{4}}{=}{2}$ (10)
 > $\mathrm{out}≔\mathrm{QuantifierElimination}\left(f,\mathrm{output}=\mathrm{rootof}\right)$
 ${\mathrm{out}}{≔}\left({\mathrm{RootOf}}{}\left({{\mathrm{_Z}}}^{{4}}{-}{2}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{1}}\right){\le }{x}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{&and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({x}{\le }{\mathrm{RootOf}}{}\left({{\mathrm{_Z}}}^{{4}}{-}{2}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right)\right)$ (11)

The output formula can be simplified optionally as follows

 > $\mathrm{ff}≔&E\left(\left[i,j\right]\right),\left(\left(\left(\left(0\le i\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&and\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}i\le n\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&and\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}0\le j\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&and\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}j\le n\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&and\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(t=n-j\right)\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&and\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(p=i+j\right)$
 ${\mathrm{ff}}{≔}{&E}{}\left(\left[{i}{,}{j}\right]\right){,}\left(\left(\left(\left(\left({0}{\le }{i}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{&and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({i}{\le }{n}\right)\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{&and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({0}{\le }{j}\right)\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{&and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({j}{\le }{n}\right)\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{&and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({t}{=}{n}{-}{j}\right)\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{&and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({p}{=}{i}{+}{j}\right)$ (12)
 > $R≔\mathrm{PolynomialRing}\left(\left[i,j,p,t,n\right]\right)$
 ${R}{≔}{\mathrm{polynomial_ring}}$ (13)
 > $\mathrm{sols}≔\mathrm{QuantifierElimination}\left(\mathrm{ff},R,\mathrm{output}=\mathrm{rootof},\mathrm{simplification}=\mathrm{false}\right)$
 ${\mathrm{sols}}{≔}{\mathrm{&or}}{}\left({\mathrm{&and}}{}\left({n}{=}{0}{,}{t}{=}{n}{,}{p}{=}{0}\right){,}{\mathrm{&and}}{}\left({0}{<}{n}{,}{t}{=}{0}{,}{p}{=}{n}\right){,}{\mathrm{&and}}{}\left({0}{<}{n}{,}{t}{=}{0}{,}{n}{<}{p}{,}{p}{<}{2}{}{n}\right){,}{\mathrm{&and}}{}\left({0}{<}{n}{,}{t}{=}{0}{,}{p}{=}{2}{}{n}\right){,}{\mathrm{&and}}{}\left({0}{<}{n}{,}{0}{<}{t}{,}{t}{<}{n}{,}{p}{=}{-}{t}{+}{n}\right){,}{\mathrm{&and}}{}\left({0}{<}{n}{,}{0}{<}{t}{,}{t}{<}{n}{,}{-}{t}{+}{n}{<}{p}{,}{p}{<}{-}{t}{+}{2}{}{n}\right){,}{\mathrm{&and}}{}\left({0}{<}{n}{,}{0}{<}{t}{,}{t}{<}{n}{,}{p}{=}{-}{t}{+}{2}{}{n}\right){,}{\mathrm{&and}}{}\left({0}{<}{n}{,}{t}{=}{n}{,}{p}{=}{0}\right){,}{\mathrm{&and}}{}\left({0}{<}{n}{,}{t}{=}{n}{,}{0}{<}{p}{,}{p}{<}{n}\right){,}{\mathrm{&and}}{}\left({0}{<}{n}{,}{t}{=}{n}{,}{p}{=}{n}\right)\right)$ (14)
 > $\mathrm{sols}≔\mathrm{QuantifierElimination}\left(\mathrm{ff},R,\mathrm{output}=\mathrm{rootof},\mathrm{simplification}=\mathrm{L4}\right)$
 ${\mathrm{sols}}{≔}{\mathrm{&and}}{}\left({0}{\le }{n}{,}{0}{\le }{t}{,}{t}{\le }{n}{,}{n}{-}{t}{\le }{p}{,}{p}{\le }{-}{t}{+}{2}{}{n}\right)$ (15)

References

 Changbo Chen, Marc Moreno Maza "An Incremental Algorithm for Computing Cylindrical Algebraic Decomposition." Proceedings of ASCM 2012, Computer Mathematics, Springer, (2014): 199-221.
 Changbo Chen, Marc Moreno Maza "Quantifier elimination by cylindrical algebraic decomposition based on regular chain." J. Symb. Comput. 75: 74-93 (2016)
 Changbo Chen, Marc Moreno Maza "Simplification of Cylindrical Algebraic Formula." Computer Algebra in Scientific Computing (CASC), Lecture Notes in Computer Science - 9301, (2015): 119-134.

Compatibility

 • The RegularChains[SemiAlgebraicSetTools][QuantifierElimination] command was introduced in Maple 2020.