# DISCOVERER: A tool for solving semi-algebraic systems

DISCOVERER is a package developed by Bican Xia using Maple language, which provides some functions for studying real solutions of semi-algebraic systems. The package is free for use in research and teaching.

The package and documentations can be downloaded here.

### Introduction

A system in the form of [P,G1,G2,H] is called a semi-algebraic system (SAS), where P=[p_1,...,p_s], G1=[g1_1,...,g1_r], G2=[g2_1,...,g2_t], H=[h_1,...,h_m] and

p_1=0,...,p_s=0,

g1_1>=0,...,g1_r>=0,

g2_1>0,...,g2_t>0,

h_1<>0,...,h_m<>0 ( ¡°<>¡± stands for "not equal").

Herein,
p(i), g1(j), g2(k), h(l) are all polynomials in Q[u,x] , u=(u_1,...,u_d) are parameters and x=(x_1,...,x_n) variables with s>0, d>=0. An SAS is called a *parametric* SAS if d>0 and a* constant* system otherwise. For a given SAS, we are interested in the following problems.

- Constant£¨d=0£©
- 1.1 Does the system have real solutions? The dimension of real solutions?;
- 1.2 If the dimension is zero, what is the number of real solutions? And, how to isolate the real solutions?

- Parametric£¨d>0£©
- 2.1 What is the condition the parameters must satisfy for the system to have real solutions?
- 2.2 What is the condition on the parameters such that dimension of real solutions of the system is positive? What is the dimension?
- 2.3 What is the necessary and sufficient condition on the parameters such that the system has a prescribed number of real solutions?

DISCOVERER can answer the questions listed above [ 1£10 ].

### Main Features

The main features of DISCOVERER include

- Real solution classifications of parametric SASs, i.e., the Problems 2.1, 2.2 and 2.3.
- Real solution isolation of constant SASs, i.e., the second part of problem 1.2.
- Real solution counting, i.e., the Problem 1.1 and the first part of Problem 1.2.
- Discriminant Sequences for Polynomials, Negative Root Discriminant Sequences for Polynomials.
- Relatively Simplicial Decomposition (RSD).
- A Partial CAD algorithm (PCAD).

About the concepts involved, please refer to [3, 5, 7, 8, 9, 10].

### Usage

The documentations can be downloaded (site1or site2) together with the package.

### References

[1] B. Xia: DISCOVERER: A tool for solving problems involving polynomial inequalities. In: Proc. ATCM'2000 (Wei-Chi Yang, et al. eds.), 472--481. ATCM Inc., lacksburg, USA, 2000.

[2] B. Xia, R. Xiao and L. Yang: Solving parametric semi-algebraic systems. In£ºProc. the 7th Asian Symposium on Computer Mathematics (ASCM 2005)}, (Sung-il Pae, H. Park, eds.), 153--156. Seoul, Dec.8-10, 2005.

[3] B. Xia and L. Yang: An algorithm for isolating the real solutions of semi-algebraic systems. J. Symb. Comput., 34: 461--477, 2002.

[4] B. Xia and T. Zhang: Algorithms for real root isolation based on interval arithmetic. Institute of Mathematics, Peking University, Research Report No. 107, 2003.

[5] B. Xia and T. Zhang: Real Solution Isolation Using Interval Arithmetic. Computers and Mathematics with Applications, 52: 853--860, 2006.

[6] L. Yang, X. Hou and B. Xia: Automated discovering and proving for geometric inequalities. In: Automated Deduction in Geometry ( X. S. Gao, D. Wang \& L. Yang eds.), LNAI 1669, Springer-Verlag, 30--46, 1999.

[7] L. Yang, X. Hou and B. Xia: A complete algorithm for automated discovering of a class of inequality-type theorems. Sci. China F 44£º33--49, 2001.

[8] L. Yang, X. Hou and Z. Zeng: A complete discrimination system for polynomials. Sci. China E 39(6) : 628--646, 1996.

[9] L. Yang and B. Xia: Automated Deduction in Geometry. In: Geometric Computation, 248--298. World Scientific, 2004.

[10] L. Yang and B. Xia: Real solution classifications of parametric semi-algebraic systems. In: Algorithmic Algebra and Logic --- Proceedings of the A3L 2005 (A. Dolzmann, A. Seidl, and T. Sturm, eds.), 281--289. Herstellung und Verlag, Norderstedt, 2005.