ÏÄ±Ú²Ó (Bican Xia)


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.


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
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

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


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


[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.

© 2007-11-27