>
|
|
>
|
|
Suppose that we would like to solve the following Quantifier Elimination (QE) problem (due to Davenport and Heintz): find a logic formula involving only and which is logically equivalent to the following formula
We first define a logic formula:
>
|
|
| (1) |
Then we invoke the QuantifierElimination command on the above formula
>
|
|
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.
>
|
|
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.
>
|
|
| (5) |
By default, QuantifierElimination returns the standard quantifier-free formula, namely the Tarski formula. Extended Tarski formulas are supported by the option output=rootof.
>
|
|
| (7) |
>
|
|
>
|
|
| (11) |
The output formula can be simplified optionally as follows
>
|
|
| (12) |
>
|
|
>
|
|
| (14) |
>
|
|
| (15) |