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.

1. 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?
2. 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.