Example Worksheet - Maple Help

All Products Maple MapleSim

Home : Support : Online Help : Mathematics : Factorization and Solving Equations : RegularChains : Quantifier Elimination : Example Worksheet

Demonstration of the QuantifierElimination and QuantifierTools packages in Maple

>	with( QuantifierElimination );

$[CylindricalAlgebraicDecompose, DeleteFormula, InsertFormula, PartialCylindricalAlgebraicDecompose, QuantifierEliminate, QuantifierTools]$

(1)

>	with( QuantifierTools );

$[AlphaConvert, ConvertRationalConstraintsToTarski, ConvertToPrenexForm, GetAllPolynomials, GetEquationalConstraints, GetUnquantifiedFormula, NegateFormula, SuggestCADOptions]$

(2)

This worksheet is an in-depth demonstration of ways to use the routines of QuantifierElimination and QuantifierTools.

Throughout, QE and CAD are abbreviations of Quantifier Elimination and Cylindrical Algebraic Decomposition, respectively.

It also offers a wealth of typical examples on how to interact with QEData and CADData objects returned in the course of incrementality or stock CAD.

QE or CAD formulae as examples that originally have an academic source are appended with a reference on formula definition (generally [3] or [9]). Both works are either repositories of data or works that cite a repository of data. Other references appended at the bottom of the worksheet are general major works of interest in terms of implementation of the QuantifierElimination package. An extremely comprehensive source of reference for the package and in particular its implementation is [8].

Quantifier Elimination & Tarski formulae

Below demonstrates some general usage of the package, in particular in terms of what to expect from QuantifierEliminate in terms of input syntax for formulae. By default, when no keyword options are used, the quantifier-free equivalent of a formula is returned.

>	expr := exists( [ x, y ], And( 3x^2 - 2y > 0, Or( x > 0, y > 0 ) ) );

$expr ≔ \exists ([x, y], 0 < 3 x^{2} - 2 y \land (0 < x \lor 0 < y))$

(1.1)

>	QuantifierEliminate( expr );

$true$

(1.2)

>	expr := exists( x, forall( y, exists( z, And(4x^2 + xy^2 - z + 1/4 = 0, 2x + y^2z + 1/2 = 0, x^2z - 1/2x - y^2 = 0 ) ) ) );

$expr ≔ \exists (x, \forall (y, \exists (z, 4 x^{2} + x y^{2} - z + \frac{1}{4} = 0 \land 2 x + y^{2} z + \frac{1}{2} = 0 \land x^{2} z - \frac{1}{2} x - y^{2} = 0)))$

(1.3)

>	QuantifierEliminate( expr );

$false$

(1.4)

Generic boolean operators such as Implies are supported. Under the hood, QuantifierElimination routines work with 'prenex' formulae only.

>	expr := Implies( forall( x, x > 0 ), x^2 > 0 );

$expr ≔ \forall (x, 0 < x) \Rightarrow 0 < x^{2}$

(1.5)

>	QuantifierEliminate( expr );

$true$

(1.6)

The conversion to prenex form can be realized by the QuantifierTools routine ConvertToPrenexForm.

>	prenexExpr := ConvertToPrenexForm( expr );

$prenexExpr ≔ \exists (x, 0 \leq - x \lor - x^{2} < 0)$

(1.7)

>	QuantifierEliminate( prenexExpr );

$true$

(1.8)

QuantifierEliminate accepts formulae involving rational functions:

>	expr := exists( x, x / y > 0 );

$expr ≔ \exists (x, 0 < \frac{x}{y})$

(1.9)

>	QuantifierEliminate( expr );

$y < 0 \lor - y < 0$

(1.10)

These rational functions are interpreted in terms of equivalent Tarski formulae under the hood. This conversion is realizable by the QuantifierTools routine ConvertRationalConstraintsToTarski:

>	ConvertRationalConstraintsToTarski( expr );

$\exists (x, 0 < x y)$

(1.11)

Witnesses for QE [5] on fully quantified formulae [3], relation to Satisfiability Modulo Theories (SMT)

For formulae where every variable is quantified in terms of exactly one quantifier symbol, the quantifier-free equivalent of the formula must be identically 'true' or 'false'.

>	expr := exists([v__1, v__2, v__3, v__4, v__5, v__6, v__7, v__8],And(v__7 < 0,0 < v__8,0 < v__4,v__2v__6+v__3v__8 = v__4,v__1v__5+v__3v__7 = v__4,v__6 = 1,v__5 = 1, 0 < v__1)); # [3], Economics QE example 0001

$expr ≔ \exists ([v__1, v__2, v__3, v__4, v__5, v__6, v__7, v__8], v__7 < 0 \land 0 < v__8 \land 0 < v__4 \land v__2 v__6 + v__3 v__8 = v__4 \land v__1 v__5 + v__3 v__7 = v__4 \land v__6 = 1 \land v__5 = 1 \land 0 < v__1)$

(2.1)

>	QuantifierEliminate( expr );

$true$

(2.2)

In the scenario where a formula is equivalent to 'true' in the existentially quantified case, or 'false' in the universally quantified case, there exists a set of assignments of the quantified variables to real algebraic numbers that realizes the equivalence of the quantified formula to its quantifier-free equivalent. This is called a set of 'witnesses'. Witnesses can be requested as an output argument by including the symbol 'witnesses' as part of the list for the keyword option 'output':

>	( q, w ) := QuantifierEliminate( expr, 'output = [ qf, witnesses]' ); # provide some witnesses for proof of the example

$q, w ≔ true, [[true, v__8 = \frac{9}{2}, v__7 = - \frac{1}{2}, v__6 = 1, v__5 = 1, v__4 = \frac{1}{4}, v__3 = \frac{1}{2}, v__2 = −2, v__1 = \frac{1}{2}]]$

(2.3)

>	wit := w[][ 2 .. -1 ];

$wit ≔ [v__8 = \frac{9}{2}, v__7 = - \frac{1}{2}, v__6 = 1, v__5 = 1, v__4 = \frac{1}{4}, v__3 = \frac{1}{2}, v__2 = −2, v__1 = \frac{1}{2}]$

(2.4)

>	map( evalb@eval, GetUnquantifiedFormula( expr ), wit ); # the witnesses work

$true \land true \land true \land true \land true \land true \land true \land true$

(2.5)

>	# evalb@eval composition of evalb with eval

>	( q, w ) := QuantifierEliminate( expr, 'output = [ qf, witnesses ]', 'processwitnesses' = false );

$q, w ≔ true, [[true, v__8 = - \frac{v__2 v__6 - v__4}{v__3}, v__7 = - \frac{v__1 v__5 - v__4}{v__3}, v__6 = 1, v__5 = 1, v__4 = ε, v__3 = ε, v__2 = - \infty, v__1 = ε]]$

(2.6)

Satisfy from the SMTLIB package offers similar functionality when judging the unquantified part of the quantified formula to be an SMT formula under the theory of real arithmetic.

>	exprUnq := GetUnquantifiedFormula( expr );

$exprUnq ≔ v__7 < 0 \land 0 < v__8 \land 0 < v__4 \land v__2 v__6 + v__3 v__8 = v__4 \land v__1 v__5 + v__3 v__7 = v__4 \land v__6 = 1 \land v__5 = 1 \land 0 < v__1$

(2.7)

>	SMTWitnesses := SMTLIB:-Satisfy( exprUnq );

$SMTWitnesses ≔ \{v__1 = \frac{17}{8}, v__2 = \frac{1}{8}, v__3 = 1, v__4 = \frac{9}{8}, v__5 = 1, v__6 = 1, v__7 = −1, v__8 = 1\}$

(2.8)

>	map( evalb@eval, exprUnq, convert( SMTWitnesses, 'list' ) );

$true \land true \land true \land true \land true \land true \land true \land true$

(2.9)

Usage of a low value for the 'eagerness' keyword option can provide a more comprehensive set of witnesses at the cost of more exploration of the solution space by the QE algorithm(s) used.

>	( q, w ) := QuantifierEliminate( expr, 'output = [ qf, witnesses ]', 'eagerness' = 1 ): # get a covering of all possible witnesses q; map(print, w):

$true$

$[true, v__8 = \frac{9}{2}, v__7 = - \frac{1}{2}, v__6 = 1, v__5 = 1, v__4 = \frac{1}{4}, v__3 = \frac{1}{2}, v__2 = −2, v__1 = \frac{1}{2}]$

$[true, v__8 = \frac{1}{2}, v__7 = - \frac{1}{2}, v__6 = 1, v__5 = 1, v__4 = \frac{1}{4}, v__3 = \frac{1}{2}, v__2 = 0, v__1 = \frac{1}{2}]$

$[true, v__8 = \frac{9}{2}, v__7 = - \frac{1}{2}, v__6 = 1, v__5 = 1, v__4 = \frac{1}{4}, v__3 = \frac{1}{2}, v__2 = −2, v__1 = \frac{1}{2}]$

$[true, v__8 = \frac{1}{2}, v__7 = - \frac{1}{2}, v__6 = 1, v__5 = 1, v__4 = \frac{1}{4}, v__3 = \frac{1}{2}, v__2 = 0, v__1 = \frac{1}{2}]$

$[true, v__8 = \frac{1}{14}, v__7 = - \frac{3}{7}, v__6 = 1, v__5 = 1, v__4 = \frac{2}{7}, v__3 = \frac{1}{2}, v__2 = \frac{1}{4}, v__1 = \frac{1}{2}]$

$[true, v__8 = \frac{1}{2}, v__7 = - \frac{1}{2}, v__6 = 1, v__5 = 1, v__4 = \frac{1}{4}, v__3 = \frac{1}{2}, v__2 = 0, v__1 = \frac{1}{2}]$

$[true, v__8 = \frac{1}{14}, v__7 = - \frac{3}{7}, v__6 = 1, v__5 = 1, v__4 = \frac{2}{7}, v__3 = \frac{1}{2}, v__2 = \frac{1}{4}, v__1 = \frac{1}{2}]$

$[true, v__8 = \frac{1}{2}, v__7 = - \frac{1}{2}, v__6 = 1, v__5 = 1, v__4 = \frac{1}{4}, v__3 = \frac{1}{2}, v__2 = 0, v__1 = \frac{1}{2}]$

$[true, v__8 = \frac{1}{14}, v__7 = - \frac{3}{7}, v__6 = 1, v__5 = 1, v__4 = \frac{2}{7}, v__3 = \frac{1}{2}, v__2 = \frac{1}{4}, v__1 = \frac{1}{2}]$

$[true, v__8 = \frac{1}{2}, v__7 = - \frac{1}{2}, v__6 = 1, v__5 = 1, v__4 = \frac{1}{4}, v__3 = \frac{1}{2}, v__2 = 0, v__1 = \frac{1}{2}]$

$[true, v__8 = \frac{1}{14}, v__7 = - \frac{3}{7}, v__6 = 1, v__5 = 1, v__4 = \frac{2}{7}, v__3 = \frac{1}{2}, v__2 = \frac{1}{4}, v__1 = \frac{1}{2}]$

$[true, v__8 = \frac{1}{21}, v__7 = - \frac{1}{28}, v__6 = 1, v__5 = 1, v__4 = \frac{4}{7}, v__3 = −2, v__2 = \frac{2}{3}, v__1 = \frac{1}{2}]$

$[true, v__8 = \frac{1}{2}, v__7 = −2, v__6 = 1, v__5 = 1, v__4 = \frac{1}{2}, v__3 = 0, v__2 = \frac{1}{2}, v__1 = \frac{1}{2}]$

(2.10)

>	for wit in w do # all witness results work map( evalb@eval, GetUnquantifiedFormula( expr ), wit[ 2.. -1 ] ); end do;

$true \land true \land true \land true \land true \land true \land true \land true$

(2.11)

Exploring a universally quantified problem equivalent to false provides the same functionality:

>	expr := forall([v__1, v__2, v__3, v__4, v__5, v__6, v__7, v__8],Implies(And(v__7 < 0,0 < v__8,0 < v__4,v__2v__6+v__3v__8 = v__4,v__1v__5+v__3v__7 = v__4,v__6 = 1, v__5 = 1),0 < v__1)); # [3], Economics QE theorem 0001

$expr ≔ \forall ([v__1, v__2, v__3, v__4, v__5, v__6, v__7, v__8], v__7 < 0 \land 0 < v__8 \land 0 < v__4 \land v__2 v__6 + v__3 v__8 = v__4 \land v__1 v__5 + v__3 v__7 = v__4 \land v__6 = 1 \land v__5 = 1 \Rightarrow 0 < v__1)$

(2.12)

>	( q, w ) := QuantifierEliminate( expr, 'output = [ qf, witnesses ]' );

$q, w ≔ false, [[false, v__8 = \frac{1}{8}, v__7 = - \frac{9}{8}, v__6 = 1, v__5 = 1, v__4 = \frac{1}{4}, v__3 = −2, v__2 = \frac{1}{2}, v__1 = −2]]$

(2.13)

>	map( evalb@eval, ConvertToPrenexForm( GetUnquantifiedFormula( expr ) ), w[][ 2.. -1 ] );

$false \lor false \lor false \lor false \lor false \lor false \lor false \lor false$

(2.14)

QE specifically requested by CAD using PartialCylindricalAlgebraicDecompose offers the same functionality as QuantifierEliminate.

>	( q, w, data ) := PartialCylindricalAlgebraicDecompose( expr, 'output = [ qf, witnesses, data ]', 'eagerness = 1' ); # CAD provides the same functionality

$q, w, data ≔ false, [[false, v__2 = 1, v__8 = 1, v__7 = −1, v__6 = 1, v__5 = 1, v__3 = - \frac{2}{3}, v__1 = - \frac{1}{3}, v__4 = \frac{1}{3}], [false, v__2 = 1, v__8 = 1, v__7 = −1, v__6 = 1, v__5 = 1, v__3 = - \frac{1}{2}, v__1 = 0, v__4 = \frac{1}{2}]], [\begin{array}{l} Variables & = & [v__2, v__8, v__7, v__6, v__5, v__3, v__1, v__4] \\ Input Formula & = & \forall ([v__2, v__8, v__7, v__6, v__5, v__3, v__1, v__4], - v__7 \leq 0 \lor v__8 \leq 0 \lor v__4 \leq 0 \lor v__2 v__6 + v__3 v__8 - v__4 \neq 0 \lor v__1 v__5 + v__3 v__7 - v__4 \neq 0 \lor v__6 - 1 \neq 0 \lor v__5 - 1 \neq 0 \lor - v__1 < 0) \\ # Cells & = & 451 \\ Projection polynomials for level 1 & = & [\begin{array}{c} v__2 \end{array}] \\ Projection polynomials for level 2 & = & [\begin{array}{c} v__8 \end{array}] \\ Projection polynomials for level 3 & = & [\begin{array}{c} v__7 & v__7 - v__8 \end{array}] \\ Projection polynomials for level 4 & = & [\begin{array}{c} v__6 & v__6 - 1 \end{array}] \\ Projection polynomials for level 5 & = & [\begin{array}{c} v__5 & v__5 - 1 \end{array}] \\ Projection polynomials for level 6 & = & [\begin{array}{c} v__3 & v__2 v__6 + v__3 v__8 & v__2 v__6 - v__3 v__7 + v__3 v__8 \end{array}] \\ Projection polynomials for level 7 & = & [\begin{array}{c} v__1 & v__1 v__5 + v__3 v__7 & v__1 v__5 - v__2 v__6 + v__3 v__7 - v__3 v__8 \end{array}] \\ Projection polynomials for level 8 & = & [\begin{array}{c} v__4 & v__2 v__6 + v__3 v__8 - v__4 & v__1 v__5 + v__3 v__7 - v__4 \end{array}] \end{array}$

(2.15)

>	map( evalb@eval, ConvertToPrenexForm( GetUnquantifiedFormula( expr ) ), w[2][ 2.. -1 ] );

$false \lor false \lor false \lor false \lor false \lor false \lor false \lor false$

(2.16)

Full incrementality for QE [1,2,4] & homogeneously quantified problems

QuantifierElimination offers the opportunity to perform QE in an entirely 'evolutionary' fashion. The word 'evolutionary' is roughly synonymous with the word 'incrementality' usually used in academic literature for QE in this context.

This means that solution of a QE problem can be performed incrementally in terms of intermediate formulae, reusing returned data structures to make successive calls adding extra parts of the formula more performant. In this way, if an intermediate quantified formula is equivalent to a fixed point (such as 'true' or 'false'), one can terminate computation early without needing to perform successive calls with extra parts of the formula.

More generally, incrementality allows for more granular and powerful inspection of quantified formulae.

The term 'evolutionary' is intended to make the definition of 'incrementality' less loose—the InsertFormula and DeleteFormula routines in QuantifierElimination strictly correspond to incrementality (addition of data to a previous formula) and decrementality (removal of data from a previous formula).

>	expr := forall( x, Implies( x > 0, x^2 > 0 ) );

$expr ≔ \forall (x, 0 < x \Rightarrow 0 < x^{2})$

(3.1)

>	forall( x, Implies( x >= 0, x^2 > 0 ) );

$\forall (x, 0 \leq x \Rightarrow 0 < x^{2})$

(3.2)

>	ConvertToPrenexForm( expr );

$\forall (x, 0 \leq - x \lor - x^{2} < 0)$

(3.3)

With a formula in prenex form, one can explore manipulation of the formula from a QE perspective. Note that the symbol 'data' must appear in the list requested for output via the keyword option 'output'. The QEData object returned contains the data structures necessary to enable further evolutionary operations via InsertFormula and DeleteFormula.

>	( q, w, data ) := QuantifierEliminate( expr, 'output = [ qf, witnesses, data ]' );

$q, w, data ≔ true, [], QEData for \forall (x, x \leq 0 \lor - x^{2} < 0)$

(3.4)

Perform QE with the operand of the quantified formula at atomic position 1 removed. In other words, we consider a change to the originally quantified formula such that 0 <= -x is removed.

Atomic positions simply refer to the position of an operand of a formula in terms of traversal of the formula as a DAG.

>	( q, w, data ) := DeleteFormula( data, 1, 'output = [ qf, witnesses, data ]' );

$q, w, data ≔ false, [[false, x = 0]], QEData for \forall (x, - x^{2} < 0)$

(3.5)

Having removed the operand 0 <= -x, we now investigate its replacement with the atomic formula x < 0. In terms of the original formula featuring the Implies symbol, the quantified formula below is equivalent to Implies( 0 <= x, 0 < x^2 ), which should be false, because of x = 0.

InsertFormula requires an operand corresponding to 'And' or 'Or', as more generally one can "build" a new disjunction or conjunction at an atomic position in usage of this parameter. Here, we are essentially rebuilding the disjunction which we lost as of the last call.

>	( q, w, data ) := InsertFormula( data, 'Or', 1, x < 0, 'output = [ qf, witnesses, data ]' );

$q, w, data ≔ false, [[false, x = 0]], QEData for \forall (x, x < 0 \lor - x^{2} < 0)$

(3.6)

Formulae which are "SMT-like" in the sense they have many variables which are all quantified with the same symbol, and are essentially a large conjunction of formulae (i.e. the formula is in conjunctive normal form) admit usage of this incrementality very well.

>	expr := exists([v__1, v__2, v__3, v__4, v__5, v__6, v__7, v__8],And(v__2 = v__1,v__3* v__5+v__4v__7 = v__1,v__3v__6+v__4v__7 = v__1,v__3v__6+v__4*v__8 = v__2,0 < v__3,0 < v__4,v__6 < v__5,v__7 < v__8)); # [3], Economics QE example 0018

$expr ≔ \exists ([v__1, v__2, v__3, v__4, v__5, v__6, v__7, v__8], v__2 = v__1 \land v__3 v__5 + v__4 v__7 = v__1 \land v__3 v__6 + v__4 v__7 = v__1 \land v__3 v__6 + v__4 v__8 = v__2 \land 0 < v__3 \land 0 < v__4 \land v__6 < v__5 \land v__7 < v__8)$

(3.7)

Eliminate the quantifiers without incrementality:

>	QuantifierEliminate( expr );

$false$

(3.8)

To instead perform QE incrementally in terms of the operands of the formula, start with the quantified formula corresponding to quantification of just the first operand:

>	exprIn := op( 0, expr )( op( 1, expr ), op( [ 2, 1 ], expr ) );

$exprIn ≔ \exists ([v__1, v__2, v__3, v__4, v__5, v__6, v__7, v__8], v__2 = v__1)$

(3.9)

>	( q, w, data ) := QuantifierEliminate( exprIn, 'output = [ qf, witnesses, data ]' );

$q, w, data ≔ true, [[true, v__2 = 0, v__3 = 0, v__4 = 0, v__5 = 0, v__6 = 0, v__7 = 0, v__8 = 0, v__1 = 0]], QEData for \exists ([v__3, v__4, v__5, v__6, v__7, v__8, v__1, v__2], v__1 - v__2 = 0)$

(3.10)

One can then do a loop to successively add in the further operands from the formula. If the quantified formula we are building is ever equivalent 'false', no addition of further operands will make the formula 'true' due to the conjunctive nature of the formula.

for i from 2 to nops( op( 2, expr ) ) do
    print( op( [ 2, i ], expr ) );
    ( q, w, data ) := InsertFormula( data, ':-And', i, op( [ 2, i ], expr ), 'output = [ qf, witnesses, data ]' );
    if q then
        print( map( is, eval( ':-And'( op( [ 2, 1 .. i ], expr ) ), w[ 1 ][ 2 .. -1 ] ) ) );
    end if;
until not q;

$v__3 v__5 + v__4 v__7 = v__1$

$q, w, data ≔ true, [[true, v__2 = 0, v__1 = 0, v__6 = 0, v__8 = 0, v__3 = 0, v__4 = 0, v__5 = 0, v__7 = 0]], QEData for \exists ([v__6, v__8, v__3, v__4, v__5, v__7, v__1, v__2], v__1 - v__2 = 0 \land - v__3 v__5 - v__4 v__7 + v__1 = 0)$

$true \land true$

$v__3 v__6 + v__4 v__7 = v__1$

$q, w, data ≔ true, [[true, v__2 = 0, v__1 = 0, v__5 = 0, v__3 = 0, v__8 = 0, v__4 = 0, v__7 = 0, v__6 = 0]], QEData for \exists ([v__8, v__4, v__7, v__6, v__3, v__5, v__1, v__2], v__1 - v__2 = 0 \land - v__3 v__5 - v__4 v__7 + v__1 = 0 \land - v__3 v__6 - v__4 v__7 + v__1 = 0)$

$true \land true \land true$

$v__3 v__6 + v__4 v__8 = v__2$

$q, w, data ≔ true, [[true, v__2 = 0, v__1 = 0, v__5 = 0, v__3 = 0, v__7 = 0, v__4 = 0, v__6 = 0, v__8 = 0]], QEData for \exists ([v__6, v__8, v__4, v__7, v__3, v__5, v__1, v__2], v__1 - v__2 = 0 \land - v__3 v__5 - v__4 v__7 + v__1 = 0 \land - v__3 v__6 - v__4 v__7 + v__1 = 0 \land - v__3 v__6 - v__4 v__8 + v__2 = 0)$

$true \land true \land true \land true$

$0 < v__3$

$q, w, data ≔ true, [[true, v__2 = 0, v__1 = 0, v__5 = 0, v__3 = \frac{1}{2}, v__7 = 0, v__4 = 0, v__6 = 0, v__8 = 0]], QEData for \exists ([v__6, v__8, v__4, v__7, v__3, v__5, v__1, v__2], v__1 - v__2 = 0 \land - v__3 v__5 - v__4 v__7 + v__1 = 0 \land - v__3 v__6 - v__4 v__7 + v__1 = 0 \land - v__3 v__6 - v__4 v__8 + v__2 = 0 \land - v__3 < 0)$

$true \land true \land true \land true \land true$

$0 < v__4$

$q, w, data ≔ true, [[true, v__2 = 0, v__1 = 0, v__5 = 0, v__3 = \frac{1}{2}, v__7 = 0, v__4 = \frac{1}{2}, v__6 = 0, v__8 = 0]], QEData for \exists ([v__6, v__8, v__4, v__7, v__3, v__5, v__1, v__2], v__1 - v__2 = 0 \land - v__3 v__5 - v__4 v__7 + v__1 = 0 \land - v__3 v__6 - v__4 v__7 + v__1 = 0 \land - v__3 v__6 - v__4 v__8 + v__2 = 0 \land - v__3 < 0 \land - v__4 < 0)$

$true \land true \land true \land true \land true \land true$

$v__6 < v__5$

$q, w, data ≔ false, [], QEData for \exists ([v__6, v__8, v__4, v__7, v__3, v__5, v__1, v__2], v__1 - v__2 = 0 \land - v__3 v__5 - v__4 v__7 + v__1 = 0 \land - v__3 v__6 - v__4 v__7 + v__1 = 0 \land - v__3 v__6 - v__4 v__8 + v__2 = 0 \land - v__3 < 0 \land - v__4 < 0 \land v__6 - v__5 < 0)$

(3.11)

$false$

(3.12)

In this case, the formula is actually equivalent to false without usage of all the operands. The unsatisfiable core of the formula is smaller than the set of all the operands.

>	i, op( [ 2, i ], expr ), op( [ 2, -1 ], expr ); # the clause where we obtained 'false', and the last clause

$7, v__6 < v__5, v__7 < v__8$

(3.13)

j := 1;

$j ≔ 1$

(3.14)

Using DeleteFormula, we can "go backwards" to remove operands (remove them from the opposite side we were appending to):

do
    print( op( [ 2, j ], expr ) );
    ( q, w, data ) := DeleteFormula( data, 1, 'output = [ qf, witnesses, data ]' );
    j++;
    if q then
        print( map( is, eval( ':-And'( op( [ 2, j .. i ], expr ) ), w[ 1 ][ 2 .. -1 ] ) ) );
    end if;
until j = nops( op( 2, expr ) ) - 1; # note these deletions happen in reverse order, ie. we're deleting the clause we started with first

$v__2 = v__1$

$q, w, data ≔ false, [], QEData for \exists ([v__6, v__8, v__4, v__7, v__3, v__5, v__1, v__2], - v__3 v__5 - v__4 v__7 + v__1 = 0 \land - v__3 v__6 - v__4 v__7 + v__1 = 0 \land - v__3 v__6 - v__4 v__8 + v__2 = 0 \land - v__3 < 0 \land - v__4 < 0 \land v__6 - v__5 < 0)$

$j ≔ 2$

$v__3 v__5 + v__4 v__7 = v__1$

$q, w, data ≔ true, [[true, v__2 = 0, v__1 = 0, v__5 = \frac{1}{2}, v__3 = \frac{1}{2}, v__4 = \frac{1}{2}, v__6 = 0, v__8 = 0, v__7 = 0]], QEData for \exists ([v__6, v__8, v__7, v__4, v__3, v__5, v__1, v__2], - v__3 v__6 - v__4 v__7 + v__1 = 0 \land - v__3 v__6 - v__4 v__8 + v__2 = 0 \land - v__3 < 0 \land - v__4 < 0 \land v__6 - v__5 < 0)$

$j ≔ 3$

$true \land true \land true \land true \land true$

$v__3 v__6 + v__4 v__7 = v__1$

$q, w, data ≔ true, [[true, v__2 = 0, v__1 = 0, v__5 = \frac{1}{2}, v__3 = \frac{1}{2}, v__4 = \frac{1}{2}, v__8 = 0, v__7 = 0, v__6 = 0]], QEData for \exists ([v__8, v__7, v__6, v__4, v__3, v__5, v__1, v__2], - v__3 v__6 - v__4 v__8 + v__2 = 0 \land - v__3 < 0 \land - v__4 < 0 \land v__6 - v__5 < 0)$

$j ≔ 4$

$true \land true \land true \land true$

$v__3 v__6 + v__4 v__8 = v__2$

$q, w, data ≔ true, [[true, v__2 = 0, v__5 = \frac{1}{2}, v__3 = \frac{1}{2}, v__4 = \frac{1}{2}, v__8 = 0, v__7 = 0, v__1 = 0, v__6 = 0]], QEData for \exists ([v__8, v__7, v__1, v__6, v__4, v__3, v__5, v__2], - v__3 < 0 \land - v__4 < 0 \land v__6 - v__5 < 0)$

$j ≔ 5$

$true \land true \land true$

$0 < v__3$

$q, w, data ≔ true, [[true, v__2 = 0, v__5 = \frac{1}{2}, v__3 = 0, v__4 = \frac{1}{2}, v__8 = 0, v__7 = 0, v__1 = 0, v__6 = 0]], QEData for \exists ([v__8, v__7, v__1, v__6, v__4, v__3, v__5, v__2], - v__4 < 0 \land v__6 - v__5 < 0)$

$j ≔ 6$

$true \land true$

$0 < v__4$

$q, w, data ≔ true, [[true, v__2 = 0, v__5 = \frac{1}{2}, v__8 = 0, v__7 = 0, v__1 = 0, v__6 = 0, v__4 = 0, v__3 = 0]], QEData for \exists ([v__8, v__7, v__1, v__6, v__4, v__3, v__5, v__2], v__6 - v__5 < 0)$

$j ≔ 7$

$\land (true)$

(3.15)

Investigate a similar occurrence but using a universally quantified formula. Note that witnesses are always being requested, and are kept up to date with the current state of the quantifier-free equivalent for the formula.

>	expr := exists([v__1, v__2, v__3, v__4, v__5, v__6, v__7, v__8],And(v__2 = v__1,v__3* v__5+v__4v__7 = v__1,v__3v__6+v__4v__7 = v__1,v__3v__6+v__4*v__8 = v__2,0 < v__3,0 < v__4,v__6 < v__5,v__7 < v__8)); # [3], Economics QE theorem 0001

(3.16)

>	( q, w, data ) := QuantifierEliminate( expr, 'output = [ qf, witnesses, data ]' );

$q, w, data ≔ false, [], QEData for \exists ([v__4, v__1, v__2, v__3, v__5, v__6, v__7, v__8], v__1 - v__2 = 0 \land - v__3 v__5 - v__4 v__7 + v__1 = 0 \land - v__3 v__6 - v__4 v__7 + v__1 = 0 \land - v__3 v__6 - v__4 v__8 + v__2 = 0 \land - v__3 < 0 \land - v__4 < 0 \land v__6 - v__5 < 0 \land v__7 - v__8 < 0)$

(3.17)

>	( q, w, data ) := DeleteFormula( data, 1, 'output = [ qf, witnesses, data ]' ); # delete -v__7 <= 0

$q, w, data ≔ false, [], QEData for \exists ([v__4, v__1, v__2, v__3, v__5, v__6, v__7, v__8], - v__3 v__5 - v__4 v__7 + v__1 = 0 \land - v__3 v__6 - v__4 v__7 + v__1 = 0 \land - v__3 v__6 - v__4 v__8 + v__2 = 0 \land - v__3 < 0 \land - v__4 < 0 \land v__6 - v__5 < 0 \land v__7 - v__8 < 0)$

(3.18)

>	( q, w, data ) := InsertFormula( data, 'Or', 1, -v__7 < 0, 'output = [ qf, witnesses, data ]' ); # insert v__7 < 0

$q, w, data ≔ true, [[true, v__8 = 3, v__7 = 2, v__6 = −2, v__5 = 0, v__3 = \frac{1}{2}, v__2 = \frac{1}{2}, v__1 = 0, v__4 = \frac{1}{2}]], QEData for \exists ([v__4, v__1, v__2, v__3, v__5, v__6, v__7, v__8], (- v__3 v__5 - v__4 v__7 + v__1 = 0 \lor - v__7 < 0) \land - v__3 v__6 - v__4 v__7 + v__1 = 0 \land - v__3 v__6 - v__4 v__8 + v__2 = 0 \land - v__3 < 0 \land - v__4 < 0 \land v__6 - v__5 < 0 \land v__7 - v__8 < 0)$

(3.19)

>	( q, w, data ) := DeleteFormula( data, 1, 'output = [ qf, witnesses, data ]' ); # delete v__7 < 0

$q, w, data ≔ true, [[true, v__8 = 3, v__7 = 2, v__6 = −2, v__5 = 0, v__3 = \frac{1}{2}, v__2 = \frac{1}{2}, v__1 = 0, v__4 = \frac{1}{2}]], QEData for \exists ([v__4, v__1, v__2, v__3, v__5, v__6, v__7, v__8], - v__3 v__6 - v__4 v__7 + v__1 = 0 \land - v__3 v__6 - v__4 v__8 + v__2 = 0 \land - v__3 < 0 \land - v__4 < 0 \land v__6 - v__5 < 0 \land v__7 - v__8 < 0)$

(3.20)

>	( q, w, data ) := DeleteFormula( data, 1, 'output = [ qf, witnesses, data ]' ); # delete v__8 <= 0

$q, w, data ≔ true, [[true, v__8 = 2, v__7 = −3, v__6 = −2, v__5 = 0, v__3 = \frac{1}{2}, v__4 = \frac{1}{2}, v__1 = 0, v__2 = 0]], QEData for \exists ([v__1, v__2, v__4, v__3, v__5, v__6, v__7, v__8], - v__3 v__6 - v__4 v__8 + v__2 = 0 \land - v__3 < 0 \land - v__4 < 0 \land v__6 - v__5 < 0 \land v__7 - v__8 < 0)$

(3.21)

>	( q, w, data ) := DeleteFormula( data, 1, 'output = [ qf, witnesses, data ]' ); # delete v__4 <= 0

$q, w, data ≔ true, [[true, v__8 = \frac{1}{2}, v__7 = 0, v__6 = −2, v__5 = 0, v__3 = \frac{1}{2}, v__4 = \frac{1}{2}, v__1 = 0, v__2 = 0]], QEData for \exists ([v__1, v__2, v__4, v__3, v__5, v__6, v__7, v__8], - v__3 < 0 \land - v__4 < 0 \land v__6 - v__5 < 0 \land v__7 - v__8 < 0)$

(3.22)

>	( q, w, data ) := DeleteFormula( data, 3, 'output = [ qf, witnesses, data ]' ); # delete -1 + v__5 <> 0

$q, w, data ≔ true, [[true, v__8 = \frac{1}{2}, v__7 = 0, v__6 = 0, v__5 = 0, v__3 = \frac{1}{2}, v__4 = \frac{1}{2}, v__1 = 0, v__2 = 0]], QEData for \exists ([v__1, v__2, v__4, v__3, v__5, v__6, v__7, v__8], - v__3 < 0 \land - v__4 < 0 \land v__7 - v__8 < 0)$

(3.23)

>	( q, w, data ) := DeleteFormula( data, 3, 'output = [ qf, witnesses, data ]' ); # delete -v__1 < 0

$q, w, data ≔ true, [[true, v__8 = 0, v__3 = \frac{1}{2}, v__4 = \frac{1}{2}, v__1 = 0, v__2 = 0, v__5 = 0, v__6 = 0, v__7 = 0]], QEData for \exists ([v__1, v__2, v__5, v__6, v__7, v__4, v__3, v__8], - v__3 < 0 \land - v__4 < 0)$

(3.24)

>	expr := exists([v__1, v__2, v__3, v__4, v__5, v__6, v__7, v__8],And(v__2 = v__1,v__3* v__5+v__4v__7 = v__1,v__3v__6+v__4v__7 = v__1,v__3v__6+v__4*v__8 = v__2,0 < v__3,0 < v__4,v__6 < v__5,v__7 < v__8)); # [3], Economics QE example 0018

(3.25)

>	( q, w, data ) := QuantifierEliminate( expr, 'output = [ qf, witnesses, data ]' );

(3.26)

>	( q, w, data ) := DeleteFormula( data, 6, 'output = [ qf, witnesses, data ]' ); # delete -v__4 < 0

(3.27)

>	( q, w, data ) := DeleteFormula( data, 5, 'output = [ qf, witnesses, data ]' ); # delete -v__3 < 0

$q, w, data ≔ true, [[true, v__8 = \frac{1}{2}, v__7 = 0, v__6 = −2, v__5 = 0, v__3 = 0, v__2 = 0, v__1 = 0, v__4 = 0]], QEData for \exists ([v__4, v__1, v__2, v__3, v__5, v__6, v__7, v__8], v__1 - v__2 = 0 \land - v__3 v__5 - v__4 v__7 + v__1 = 0 \land - v__3 v__6 - v__4 v__7 + v__1 = 0 \land - v__3 v__6 - v__4 v__8 + v__2 = 0 \land v__6 - v__5 < 0 \land v__7 - v__8 < 0)$

(3.28)

>	( q, w, data ) := InsertFormula( data, 'And', 5, -v__3 <= 0, 'output = [ qf, witnesses, data ]' ); # insert -v__3 <= 0

(3.29)

>	( q, w, data ) := InsertFormula( data, 'And', 6, -v__4 <= 0, 'output = [ qf, witnesses, data ]' ); # insert -v__4 <= 0

(3.30)

Get the current corresponding quantified formula for the QEData in terms of the evolutionary operations performed:

>	expr := GetInputFormula( data );

$expr ≔ \exists ([v__4, v__1, v__2, v__3, v__5, v__6, v__7, v__8], v__1 - v__2 = 0 \land - v__3 v__5 - v__4 v__7 + v__1 = 0 \land - v__3 v__6 - v__4 v__7 + v__1 = 0 \land - v__3 v__6 - v__4 v__8 + v__2 = 0 \land - v__3 \leq 0 \land - v__4 \leq 0 \land v__6 - v__5 < 0 \land v__7 - v__8 < 0)$

(3.31)

Check the current witnesses are correct:

>	map( is@eval, ConvertToPrenexForm( GetUnquantifiedFormula( expr ) ), w[1][2..-1] );

$true \land true \land true \land true \land true \land true \land true \land true$

(3.32)

>	map( eval, ConvertToPrenexForm( GetUnquantifiedFormula( expr ) ), w[1][2..-1] );

$0 = 0 \land 0 = 0 \land 0 = 0 \land 0 = 0 \land 0 \leq 0 \land 0 \leq 0 \land −2 < 0 \land - \frac{1}{2} < 0$

(3.33)

Due to the default poly-algorithm used by QuantifierEliminate, InsertFormula and DeleteFormula, evolutionary operations are only supported for QEData when the problem is homogeneously quantified as the examples above. For evolutionary methods in any context, QE by CAD must be used in isolation. The following demonstrates examples of this, by acquiring a CADData object from PartialCylindricalAlgebraicDecompose. PartialCylindricalAlgebraicDecompose performs QE purely by CAD. A CADData object is amenable to usage of InsertFormula and DeleteFormula with the same syntax as QEData otherwise.

>	expr := exists(z,forall(y,exists(x,And(4x^2+xy^2-z+1/4 = 0,2x+y^2z+1/2 = 0,x^2z-1/ 2x-y^2 = 0)))); # [9], "Random A", QEExamples

$expr ≔ \exists (z, \forall (y, \exists (x, 4 x^{2} + x y^{2} - z + \frac{1}{4} = 0 \land 2 x + y^{2} z + \frac{1}{2} = 0 \land x^{2} z - \frac{1}{2} x - y^{2} = 0)))$

(3.34)

>	op( [ 2, 2, 2 ], expr ); # the unquantified conjunction from the formula

$4 x^{2} + x y^{2} - z + \frac{1}{4} = 0 \land 2 x + y^{2} z + \frac{1}{2} = 0 \land x^{2} z - \frac{1}{2} x - y^{2} = 0$

(3.35)

>	exprIn := exists( z, forall( y, exists( x, 4x^2 + xy^2 - z + 1/4 = 0 ) ) );

$exprIn ≔ \exists (z, \forall (y, \exists (x, 4 x^{2} + x y^{2} - z + \frac{1}{4} = 0)))$

(3.36)

>	( q, w, data ) := PartialCylindricalAlgebraicDecompose( exprIn, 'output = [ qf, witnesses, data ]' );

$q, w, data ≔ true, [[true, z = −1, y = −4, x = RootOf (16 {_Z}^{2} + 64_Z + 5, - \frac{578532164786941965111}{147573952589676412928} .. - \frac{2314128659147767860417}{590295810358705651712})], [true, z = −1, y = RootOf ({_Z}^{4} - 20, - \frac{18601471984473}{8796093022208} .. - \frac{9300735992223}{4398046511104}), x = - \frac{{RootOf ({_Z}^{4} - 20, - \frac{18601471984473}{8796093022208} .. - \frac{9300735992223}{4398046511104})}^{2}}{8}], [true, z = \frac{1}{4}, y = −1, x = - \frac{1}{4}], [true, z = \frac{1}{4}, y = 0, x = 0], [true, z = \frac{1}{4}, y = 1, x = - \frac{1}{4}]], [\begin{array}{l} Variables & = & [z, y, x] \\ Input Formula & = & \exists (z, \forall (y, \exists (x, 4 x y^{2} + 16 x^{2} - 4 z + 1 = 0))) \\ # Cells & = & 11 \\ Projection polynomials for level 1 & = & [\begin{array}{c} 4 z - 1 \end{array}] \\ Projection polynomials for level 2 & = & [\begin{array}{c} y^{4} + 16 z - 4 \end{array}] \\ Projection polynomials for level 3 & = & [\begin{array}{c} 4 x y^{2} + 16 x^{2} - 4 z + 1 \end{array}] \end{array}$

(3.37)

for i from 2 to nops( op( [ 2, 2, 2 ], expr ) ) do # demonstrating incrementality with loop
    printf( "Adding clause %a\n", op( [ 2, 2, 2, i ], expr ) );
    ( q, data ) := InsertFormula( data, ':-And', i, op( [ 2, 2, 2, i ], expr ), 'output = [ qf, data ]' );
    printf( "Number of leaf cells in CAD: %d\n", NumberOfLeafCells( data ) );
until not q: # because of the innermost quantifier which is universal

Adding clause 2*x+y^2*z+1/2 = 0
Number of leaf cells in CAD: 61

>	i, nops( op( [ 2, 2, 2 ], expr ) );

$2, 3$

(3.38)

data;

$[\begin{array}{l} Variables & = & [z, y, x] \\ Input Formula & = & \exists (z, \forall (y, \exists (x, 4 x y^{2} + 16 x^{2} - 4 z + 1 = 0 \land 2 y^{2} z + 4 x + 1 = 0))) \\ # Cells & = & 61 \\ Projection polynomials for level 1 & = & [\begin{array}{c} z & 2 z - 1 & 4 z - 1 & 64 z^{3} - 48 z^{2} + 8 z + 1 \end{array}] \\ Projection polynomials for level 2 & = & [\begin{array}{c} 2 y^{2} z + 1 & y^{4} + 16 z - 4 & 4 y^{4} z^{2} - 2 y^{4} z + 4 y^{2} z - y^{2} - 4 z + 2 \end{array}] \\ Projection polynomials for level 3 & = & [\begin{array}{c} 2 y^{2} z + 4 x + 1 & 4 x y^{2} + 16 x^{2} - 4 z + 1 \end{array}] \end{array}$

(3.39)

>	q, data, NumberOfLeafCells( data );

$false, [\begin{array}{l} Variables & = & [z, y, x] \\ Input Formula & = & \exists (z, \forall (y, \exists (x, 4 x y^{2} + 16 x^{2} - 4 z + 1 = 0 \land 2 y^{2} z + 4 x + 1 = 0))) \\ # Cells & = & 61 \\ Projection polynomials for level 1 & = & [\begin{array}{c} z & 2 z - 1 & 4 z - 1 & 64 z^{3} - 48 z^{2} + 8 z + 1 \end{array}] \\ Projection polynomials for level 2 & = & [\begin{array}{c} 2 y^{2} z + 1 & y^{4} + 16 z - 4 & 4 y^{4} z^{2} - 2 y^{4} z + 4 y^{2} z - y^{2} - 4 z + 2 \end{array}] \\ Projection polynomials for level 3 & = & [\begin{array}{c} 2 y^{2} z + 4 x + 1 & 4 x y^{2} + 16 x^{2} - 4 z + 1 \end{array}] \end{array}, 61$

(3.40)

>	infolevel[ PartialCylindricalAlgebraicDecompose ] := 4:

>	( q, data ) := PartialCylindricalAlgebraicDecompose( expr, 'output = [ qf, data ]' ):

projectAllOrders: Exact triangular system deduced for equational constraints

projectAllOrders: 3 elements in Groebner basis for equational constraints

PartialCylindricalAlgebraicDecompose: Prenex conversion of input formula: exists(z,forall(y,exists(x,And(4*x*y^2+16*x^2-4*z+1 = 0,2*y^2*z+4*x+1 = 0,2*x^2*z-2*y^2-x = 0))))

PartialCylindricalAlgebraicDecompose: 2 polynomials used in restricted projection operations due to equational constraints

PartialCylindricalAlgebraicDecompose: 4 polynomials in projection basis for z

PartialCylindricalAlgebraicDecompose: 1 polynomials in projection basis for y

PartialCylindricalAlgebraicDecompose: 1 polynomials in projection basis for x

PartialCylindricalAlgebraicDecompose: 6 total polynomials in projection

PartialCylindricalAlgebraicDecompose: 111 total cells created in CAD

PartialCylindricalAlgebraicDecompose: 45 leaf cells on termination

>	q, data, NumberOfLeafCells( data );

$false, [\begin{array}{l} Variables & = & [z, y, x] \\ Input Formula & = & \exists (z, \forall (y, \exists (x, 4 x y^{2} + 16 x^{2} - 4 z + 1 = 0 \land 2 y^{2} z + 4 x + 1 = 0 \land 2 x^{2} z - 2 y^{2} - x = 0))) \\ # Cells & = & 45 \\ Projection polynomials for level 1 & = & [\begin{array}{c} z - 1 & 37104 z^{6} - 600 z^{5} + 2111 z^{4} + 122062 z^{3} + 232833 z^{2} - 680336 z + 288814 & 76752 z^{6} - 1272 z^{5} + 4197 z^{4} + 251555 z^{3} + 481837 z^{2} - 1407741 z + 595666 & 16 z^{6} + 8 z^{5} + 9 z^{4} + 61 z^{3} + 136 z^{2} - 206 z + 60 \end{array}] \\ Projection polynomials for level 2 & = & [\begin{array}{c} - 76752 z^{6} + 1272 z^{5} - 4197 z^{4} - 251555 z^{3} + 1988 y^{2} - 481837 z^{2} + 1407741 z - 595666 \end{array}] \\ Projection polynomials for level 3 & = & [\begin{array}{c} 37104 z^{6} - 600 z^{5} + 2111 z^{4} + 122062 z^{3} + 232833 z^{2} + 3976 x - 680336 z + 288814 \end{array}] \end{array}, 45$

(3.41)

>	infolevel[ PartialCylindricalAlgebraicDecompose ] := 0:

Poly-algorithmic QE [5,6]

The implementation of the default routine offered for QE in QuantifierElimination, QuantifierEliminate, is a poly-algorithm between two main algorithms for QE: VTS (Virtual Term Substitution) and CAD (Cylindrical Algebraic Decomposition).

Briefly, because VTS is currently only applicable up to certain polynomial degrees, CAD can be used as a failover when VTS is no longer applicable in intermediate processing of the formula. However, the usage of CAD within the poly-algorithm is highly incremental at such stages by default.

>	expr := exists([a, b, c, d],And(a^2+b^2 = r^2,0 <= a,b < 0,1 <= c,d < -1,c-(1+b)(c-a) = 0,d-(1-a)(d-b) = 0)); # [9], "Piano Movers Problem (Wang)", QEExamples

$expr ≔ \exists ([a, b, c, d], a^{2} + b^{2} = r^{2} \land 0 \leq a \land b < 0 \land 1 \leq c \land d < −1 \land c - (1 + b) (c - a) = 0 \land d - (1 - a) (d - b) = 0)$

(4.1)

Most QuantifierElimination routines offer printing of verbose information via infolevel.

>	infolevel[ QuantifierEliminate ] := 3;

${infolevel}_{QuantifierEliminate} ≔ 3$

(4.2)

Usage of the poly-algorithm is controllable via keyword options. The 'hybridmode' option controls how the algorithm should traverse nodes of the VTS tree when switching to CAD:

>	QuantifierEliminate( expr, 'hybridmode = depth' ); # actually default option in QuantifierEliminate

QuantifierEliminate: Prenex conversion of input formula: exists([a, b, c, d],And(a^2+b^2-r^2 = 0,-a <= 0,b < 0,-c <= -1,d < -1,a*b-b*c+a = 0,a*b-a*d-b = 0))

QuantifierEliminate: All quantifiers are the same: exists, so problem is amenable to poly-algorithmic QE

QuantifierEliminate: Eliminating last block of quantifiers in a formula exists([a, b, c, d],And(a^2+b^2-r^2 = 0,-a <= 0,b < 0,-c <= -1,d < -1,a*b-b*c+a = 0,a*b-a*d-b = 0)) via poly-algorithmic QE

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(b,0 < b) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(b,0 < -b) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < -a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(b,0 < b) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(b,0 < -b) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

QuantifierEliminate: 0 unused calculated VTS test points

QuantifierEliminate: 2 leaf formulae on termination of VTS

QuantifierEliminate: Entering CAD for the first time to solve QE problem(s) of excessive degree for VTS

QuantifierEliminate: Producing new CAD on QE problem of excessive degree: exists(a,And(a^2-r^2 <= 0,a <> 0,-a <= 0,a^2-r^2 < 0,Or(And(a^2 < 0,-a^6+a^4*r^2+2*a^5-2*a^3*r^2-2*a^4+a^2*r^2 < 0),And(-a^2+a <= 0,Or(a^2 < 0,a^6-a^4*r^2-2*a^5+2*a^3*r^2+2*a^4-a^2*r^2 < 0))),a^2-r^2 = 0,-a^2 <= 0,a^4-a^2*r^2+a^2 = 0))

QuantifierEliminate: 1 polynomials used in restricted projection operations due to equational constraints

QuantifierEliminate: 1 polynomials in projection basis for a

QuantifierEliminate: 5 polynomials in projection basis for a

QuantifierEliminate: 6 total polynomials in projection

QuantifierEliminate: 30 total cells created in CAD

QuantifierEliminate: 27 leaf cells on termination

QuantifierEliminate: Modifying existing CAD to solve QE problem of excessive degree: exists(a,And(a^2-r^2 <= 0,a^2-r^2 <> 0,a <> 0,-a <= 0,a^2-r^2 < 0,Or(And(a^3-a*r^2-a^2+r^2 <= 0,-a^6+2*a^4*r^2-a^2*r^4+2*a^5-4*a^3*r^2+2*a*r^4-2*a^4+3*a^2*r^2-r^4 <= 0),And(a <= 0,a^6-2*a^4*r^2+a^2*r^4-2*a^5+4*a^3*r^2-2*a*r^4+2*a^4-3*a^2*r^2+r^4 <= 0)),Or(And(a^2 < 0,-a^6+a^4*r^2+2*a^5-2*a^3*r^2-2*a^4+a^2*r^2 < 0),And(-a^2+a <= 0,Or(a^2 < 0,a^6-a^4*r^2-2*a^5+2*a^3*r^2+2*a^4-a^2*r^2 < 0)))))

modifyCADResult: 0 new quantified variables involved in CAD in VTS to CAD incrementality

modifyCADResult: 1 polynomials are used in restricted projection operations due to equational constraints

modifyCADResult: 4 new polynomials in r from incremental projection

modifyCADResult: 0 new polynomials in a from incremental projection

modifyCADResult: 168 total cells created in CAD

modifyCADResult: 135 leaf cells on termination

QuantifierEliminate: Modifying existing CAD to solve QE problem of excessive degree: exists(a,And(a^2-r^2 <= 0,a^2-r^2 <> 0,-a <= 0,a^2-r^2 < 0,Or(And(a^3-a*r^2-a^2+r^2 <= 0,-a^6+2*a^4*r^2-a^2*r^4+2*a^5-4*a^3*r^2+2*a*r^4-2*a^4+3*a^2*r^2-r^4 <= 0),And(a <= 0,a^6-2*a^4*r^2+a^2*r^4-2*a^5+4*a^3*r^2-2*a*r^4+2*a^4-3*a^2*r^2+r^4 <= 0)),a = 0,a^4-a^2*r^2-2*a^3+2*a*r^2+a^2-r^2 = 0))

modifyCADResult: 0 new quantified variables involved in CAD in VTS to CAD incrementality

modifyCADResult: 1 polynomials are used in restricted projection operations due to equational constraints

modifyCADResult: 0 new polynomials in r from incremental projection

modifyCADResult: 0 new polynomials in a from incremental projection

modifyCADResult: 168 total cells created in CAD

modifyCADResult: 143 leaf cells on termination

QuantifierEliminate: Modifying existing CAD to solve QE problem of excessive degree: exists(a,And(a^2-r^2 <= 0,a <> 0,-a <= 0,a^2-r^2 < 0,Or(And(a^2 < 0,-a^6+a^4*r^2+2*a^5-2*a^3*r^2-2*a^4+a^2*r^2 < 0),And(-a^2+a <= 0,Or(a^2 < 0,a^6-a^4*r^2-2*a^5+2*a^3*r^2+2*a^4-a^2*r^2 < 0))),-a^2+a <= 0,a^4-a^2*r^2-2*a^3+2*a*r^2+2*a^2-r^2 = 0))

modifyCADResult: 0 new quantified variables involved in CAD in VTS to CAD incrementality

modifyCADResult: 1 polynomials are used in restricted projection operations due to equational constraints

modifyCADResult: 0 new polynomials in r from incremental projection

modifyCADResult: 0 new polynomials in a from incremental projection

modifyCADResult: 168 total cells created in CAD

modifyCADResult: 143 leaf cells on termination

QuantifierEliminate: Modifying existing CAD to solve QE problem of excessive degree: exists(a,And(a^2-r^2 <= 0,-a <= 0,a^2-r^2 < 0,-a^2+a <= 0,a^4-a^2*r^2-2*a^3+2*a*r^2+2*a^2-r^2 = 0,a = 0,a^4-a^2*r^2-2*a^3+2*a*r^2+a^2-r^2 = 0))

modifyCADResult: 0 new quantified variables involved in CAD in VTS to CAD incrementality

modifyCADResult: 1 polynomials are used in restricted projection operations due to equational constraints

modifyCADResult: 0 new polynomials in r from incremental projection

modifyCADResult: 0 new polynomials in a from incremental projection

modifyCADResult: 168 total cells created in CAD

modifyCADResult: 143 leaf cells on termination

QuantifierEliminate: Modifying existing CAD to solve QE problem of excessive degree: exists(a,And(a < 1,a^2-a <> 0,a^4-a^2*r^2-2*a^3+2*a*r^2+2*a^2-r^2 = 0,-a <= 0,-a^2+a < 0,a = 0))

modifyCADResult: 0 new quantified variables involved in CAD in VTS to CAD incrementality

modifyCADResult: 1 polynomials are used in restricted projection operations due to equational constraints

modifyCADResult: 0 new polynomials in r from incremental projection

modifyCADResult: 0 new polynomials in a from incremental projection

modifyCADResult: 168 total cells created in CAD

modifyCADResult: 143 leaf cells on termination

QuantifierEliminate: Modifying existing CAD to solve QE problem of excessive degree: exists(a,And(-a < -1,a^2-a <> 0,a^4-a^2*r^2-2*a^3+2*a*r^2+2*a^2-r^2 = 0,-a <= 0,-a^2+a < 0,a = 0))

modifyCADResult: 0 new quantified variables involved in CAD in VTS to CAD incrementality

modifyCADResult: 1 polynomials are used in restricted projection operations due to equational constraints

modifyCADResult: 0 new polynomials in r from incremental projection

modifyCADResult: 0 new polynomials in a from incremental projection

modifyCADResult: 168 total cells created in CAD

modifyCADResult: 143 leaf cells on termination

QuantifierEliminate: Modifying existing CAD to solve QE problem of excessive degree: exists(a,And(a-1 <> 0,a^4-a^2*r^2-2*a^3+2*a*r^2+2*a^2-r^2 = 0,-a <= 0,-a^2+a < 0,a = 0))

modifyCADResult: 0 new quantified variables involved in CAD in VTS to CAD incrementality

modifyCADResult: 1 polynomials are used in restricted projection operations due to equational constraints

modifyCADResult: 0 new polynomials in r from incremental projection

modifyCADResult: 0 new polynomials in a from incremental projection

modifyCADResult: 168 total cells created in CAD

modifyCADResult: 143 leaf cells on termination

$(- r^{2} \leq 0 \land - r^{2} < 0 \land r^{2} = 0) \lor r - RootOf ({_Z}^{2} - 8, - \frac{796131459065725}{281474976710656} .. - \frac{1592262918131423}{562949953421312}) < 0 \lor RootOf ({_Z}^{2} - 8, \frac{208701085205324515393}{73786976294838206464} .. \frac{417402170410649030813}{147573952589676412928}) - r < 0$

(4.3)

>	QuantifierEliminate( expr, 'hybridmode = whole' );

QuantifierEliminate: Prenex conversion of input formula: exists([a, b, c, d],And(a^2+b^2-r^2 = 0,-a <= 0,b < 0,-c <= -1,d < -1,a*b-b*c+a = 0,a*b-a*d-b = 0))

QuantifierEliminate: All quantifiers are the same: exists, so problem is amenable to poly-algorithmic QE

QuantifierEliminate: Eliminating last block of quantifiers in a formula exists([a, b, c, d],And(a^2+b^2-r^2 = 0,-a <= 0,b < 0,-c <= -1,d < -1,a*b-b*c+a = 0,a*b-a*d-b = 0)) via poly-algorithmic QE

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(b,0 < b) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(b,0 < -b) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

ModuleCopy: 1 leaf formulae on termination of VTS

ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE

ModuleCopy: 0 unused calculated VTS test points

Maple

Maple Add-Ons

MapleSim

MapleSim Add-Ons

Systems Engineering

Consulting Services

Maple T.A. and Möbius

Education

Industries

Automotive and Aerospace

Robotics

Machine Design & Industrial Automation

Other

Application Areas

Product Pricing

Purchasing

Institutional Student Licensing

Maplesoft Elite Maintenance (EMP)

Support

Product Training

Online Product Help

Webinars & Events

Publications

Content Hubs

Examples & Applications

Community

About Maplesoft

Media Center

User Community

Contact

Online Help

All Products Maple MapleSim

Maple

Powerful math software that is easy to use

Maple Add-Ons

MapleSim

Advanced System Level Modeling

MapleSim Add-Ons

Systems Engineering

Consulting Services

Maple T.A. and Möbius

Education

Industries

Automotive and Aerospace

Robotics

Machine Design & Industrial Automation

Other

Application Areas

Product Pricing

Purchasing

Institutional Student Licensing

Maplesoft Elite Maintenance (EMP)

Support

Product Training

Online Product Help

Webinars & Events

Publications

Content Hubs

Examples & Applications

Community

About Maplesoft

Media Center

User Community

Contact

Online Help

All Products Maple MapleSim