Generating Polynomial Invariants with DISCOVERER and QEPCAD - Formal Methods and Hybrid Real-Time Systems - page 73

The above three steps constitute the main part of the algorithm in [31,34,27],
which, for any input SAS S , outputs the so-called border polynomial BP and a
quantifier-free formula Ψ in terms of polynomials in parameters u (and possible
some variables) such that, provided BP =0 , Ψ is the necessary and sucient
condition for S to have the given number (possibly infinite) of real solutions.
Since BP is a polynomial in parameters, BP =0 canbeviewedasadegenerated
condition. Therefore, the outputs of the above three steps can be read as “if
BP

=0 , the necessary and sucient condition for S to have the given number
(possibly infinite) of real solutions is Ψ .”

Remark 1. If we want to discuss the case when parameters degenerate, i.e.,
BP = 0, we put BP = 0 (or some of its factors) into the system and apply
a similar procedure to handle the new SAS.

Example 4. By the steps described above, we obtain the necessary and sucient
condition for S to have one distinct real solution is b 2

b 4 − 4 b 2 +2 < 0 − 2 < 0 ∧

provided BP =0 . Now, if b 2

− 2 = 0, adding the equation into the system, we

obtain a new SAS: [[ b 2

− 2 ,p 1 ,p 2 ,p 3 ] , [] , G 2 , []] . By the algorithm in [28,29], we
know the system has no real solutions.

2.3 A Computer Algebra Tool: DISCOVERER
We have implemented the above algorithm and some other algorithms in Maple
as a computer algebra tool, named DISCOVERER. The reader can download the
tool for free via “ http://www.is.pku.edu.cn/~xbc/discoverer.html ”. The
prerequisite to run the package is Maple 7.0 or a later version of it.
The main features of DISCOVERER include
Real Solution Classification of Parametric Semi-algebraic Systems
For a parametric SAS T of the form (1) and an argument N ,where N is one
of the following three forms:
- a non-negative integer b ;
- a range b..c ,where b, c are non-negative integers and b<c ;
- a range b..w ,where b is a non-negative integer and w is a name without
value, standing for + ∞ ,
DISCOVERER can determine the conditions on u such that the number of
the distinct real solutions of T equals to N if N is an integer, otherwise falls
in the scope N . This is by calling

tofind ([ P ] , [ G 1 ] , [ G 2 ] , [ H ] , [ x 1 , ..., x s ] , [ u 1 , ..., u t ] ,N ) ,

and results in the necessary and sucient condition as well as the border
polynomial BP of T in u such that the number of the distinct real solutions
of T exactly equals to N or belongs to N provided BP =0 . If T has infinite
real solutions for generic value of parameters, BP mayhavesomevariables.
Then, for the “boundaries” produced by “ tofind ”, i.e. BP =0 ,wecancall
Tofind ([ P ,BP ] , [ G 1 ] , [ G 2 ] , [ H ] , [ x 1 , ..., x s ] , [ u 1 , ..., u t ] ,N )

to obtain some further conditions on the parameters.