软件介绍
所谓半代数系统是指形如 [P,G1,G2,H] 的一个系统，其中
P=[p_1,...,p_s]、G1=[g1_1,...,g1_r]、G2=[g2_1,...,g2_t]、H=[h_1,...,h_m]，
且：
p_1=0,...,p_s=0、
g1_1>=0,...,g1_r>=0、
g2_1>0,...,g2_t>0、
h_1<>0,...,h_m<>0（“<>”代表不等于），
这里 p(i), g1(j), g2(k), h(l) 都是有理系数多项式环 Q[u,x] 上的多项式，u=(u_1,...,u_d) 是参数，x=(x_1,...,x_n) 是变元，并满足 等于0 的多项式的个数 s>0，参数个数 d>=0。视 d>0 或 d=0 而分别称系统是参系数的或常系数的。对给定的半代数系统，我们主要关心如下问题：
- 常系数情形（d=0）
- 1.1 系统有无实解；实解的维数；
- 1.2 零维（仅有有限个实解）时，实解的个数；（某种意义下的）精确解，即实解隔离；
- 参系数情形（d>0）
- 2.1 参数满足什么（充要）条件时，系统有实解；
- 2.2 参数满足什么（充要）条件时，系统有正维数实解，解的维数；
- 2.3 参数满足什么（充要）条件时，系统有指定数目的实解。
早在1996年，当杨路、侯晓荣、曾振炳合作首次给出多项式判别系统的科研成果【14】后，曾振炳就开发了一个 Maple 软件包 INVENTOR。这个软件包在研究半代数系统的实解时实际上并没有使用多项式判别式序列和判别系统（虽然其中包含一个由杨路编写的简练而高效的计算多项式判别式序列的程序 discr），而且功能很单一，只能用于产生参系数半代数系统存在实解的必要条件（在不考虑一些边界的前提下）。1997年，夏壁灿开始在杨路的指导下研究半代数系统的求解算法，并在 INVENTOR 的基础上开发了一个全新的研究半代数系统实解的软件包——DISCOVERER。经过近10年的开发、调试、不断增加新功能、推出新版本，目前的 DISCOVERER 已经能回答上面关于半代数系统实解的所有问题【7－13，15－17】。 自2008年起，DISCOVEREER已经集成到著名的计算机代数系统Maple之中，用户可以在Maple13以后的版本中直接调用DISCOVERER的主要功能。目前，DISCOVERER已经成为求解半代数系统的主要工具之一，也是唯一一个可以全自动求解参系数半代数系统实解分类问题的软件。我们的研究团队（包括国外的合作者以及Maple的科研人员）一直在致力于从理论和实现两方面改进我们的工具，在最新版的Maple15中，最近两年的新成果也已经融合其中，软件的效率有相当的提升。
DISCOVERER 中用到了吴文俊先生的零点分解算法【6】。从我们一开始开发 DISCOVERER 时，就使用王定康编写的实现吴零点分解的 Maple 程序 WSOLVE【2，3】。我们目前使用的还是这个较早版本的 WSOLVE，其中部分程序来自王东明的 CHARSETS 软件包【4】。因为我们只使用 WSOLVE 的部分功能，所以只保留了那部分我们会用到的函数，同时为了与 Maple 的高级版本兼容并方便我们使用，我们做了一些修改。因此准确地说，我们是利用原WSOLVE的一些函数进行了改造，现在的输出已经不同于原来的WSOLVE了。
DISCOVERER 中还直接使用了两个由张頲编写的程序：Trealroot 和 realzeros【19，10，11】。实际上，这是两个包含很多子程序的主程序，分别用于隔离一元多项式的实根和常系数半代数系统的实解。前者是张頲工作后独立编写的，后者是他在夏壁灿指导下攻读硕士学位时编写的。
DISCOVERER 从开发之初至今，一直为众多不同领域的学者、研究生所使用。他们为 DISCOVERER 的改进和完善提出了许多宝贵的意见。我们真诚地欢迎 DISCOVERER 的使用者与我们沟通：反映程序的 bug，介绍您的研究问题或提出对程序的要求。
主要功能
DISCOVERER的主要功能包括：
- 参系数半代数系统的实解分类：所谓实解分类是指上述的问题2.1、问题2.2和问题2.3。
- 常系数半代数系统的实解隔离：上述问题1.2的后半部分。
- 常系数半代数系统的实解计数：上述问题1.1及问题1.2的前半部分。
- 多项式的判别式序列、负根判别式序列、广义判别式序列。
- 相对单纯分解算法。
- 部分的柱形代数分解算法（PCAD）。
关于上面一些概念的解释，可参考【5，13，17，18】。
使用方法
DISCOVERER 在 Maple 环境下运行，要求 Maple 的版本在 7 以上。详情请见与软件包一起下载的说明文档和一个Maple下的演示工作卷。
- tofind
对于一个给定的形如 [P,G1,G2,H] 的参系数半代数系统，可以通过调用
tofind ( [P], [G1], [G2], [H], [x_1,...,x_n], [u_1,...,u_d], alpha );
来得到其实解分类。这里 alpha 可以有3种输入：1）一个非负整数 a，表示求系统恰有 a 个互异实解的条件； 2）一个范围 a..b，其中 a<b 都是非负整数，表示求系统恰有 a 到 b 个互异实解的条件；3）一个范围 a..w，其中 a 是非负整数而 w 是一个没有值的名称，表示求系统有 a 个以上互异实解的条件。特别地，输入 1..w，表示求系统有实解的条件。
程序每个主要步骤的运算都有相应的输出，且易于理解。最终的输出是一个无量词公式 phi 和一个多项式 BP，表示在 BP<>0 的前提下，系统具有所求数目实解的充要条件是 phi 为真。需要注意的是，当系统有正维数实解时，公式 phi 中可能含有一些变元；要得到关于参数的条件，需要进一步做量词消去。
- Tofind
对于由 tofind 产生的所谓“边界”，即 BP=0，我们可以把 BP 的因子逐个加入原系统来进一步计算，以判断当 BP=0 时系统实解的情况。比如设 R1 是 BP 的一个因子，则调用
Tofind ( [R1,P], [G1], [G2], [H], [x_1,...,x_n], [u_1,...,u_d], alpha);
可以得到当 R1=0 时系统有所求数目实解的充要条件。这里 alpha 的取值同上。
- realzeros
隔离常系数系统 [P,G1,G2,H] 的实解，调用方式：
realzeros ( [P], [G1], [G2], [H], [x_1,...,x_n] );
也可以要求最后输出的“方体”的最大“边长”不超过 w，这时输入
realzeros ( [P], [G1], [G2], [H], [x_1,...,x_n], w );
- nearsolve
求常系数系统 [P,G1,G2,H] 的实解数，调用方式：
nearsolve ( [P], [G1], [G2], [H], [x_1,...,x_n] );
这个命令并不需要先隔离实解。
- Trealroot
这是张颋编写的隔离一元多项式实根的程序，调用方式：
1) Trealroot(一元多项式 )；求全部解
2) Trealroot(一元多项式, 精度 )； 求全部解，要求精度,输出结果区间宽度小于精度
3) Trealroot(一元多项式, 区间 )； 求给定区间内的全部解
4) Trealroot(一元多项式, 精度, 区间 ) 或 Trealroot(一元多项式, 区间, 精度 ) ； 求给定区间内,满足精度要求的全部解
- discr, discrg, nrd
调用方式：
discr ( f, x );
discrg ( f, g, x );
nrd ( f, x );
分别求多项式 f 的判别式序列、关于 g 的广义判别式序列、负根判别式序列。
- rsd
调用方式：
rsd ( T, f, [x_1,...,x_n] );
做三角列 T 关于多项式 f 的单纯分解。
- PCAD
调用方式：
PCAD ( A, [B_1,...,B_r], [x_1,...,x_n] );
其中 A,B(i) 是多项式。做部分的柱形代数分解，输出满足 B_1>0,...,B_r>0 的 A-符号不变的柱形代数样本（不包含 A=0 的点）。
参考文献
【1】 K. O. Geddes, S.R. Czapor and G. Labahn: Algorithms for Computer Algebra. Kluwer, Boston, 1992.
【2】高小山,王定康,裘宗燕,杨宏: 方程求解与机器证明——基于MMP的问题求解. 科学出版社, 2006年.
【3】Dingkang Wang: Zero Decompostion Algorithms for Systems of Polynomial Equations. In: Proc. ASCM2000 (Gao, X.-S., Wang, D. M., eds.), World Scientific, 2000.
【4】Dongming Wang: Elimination Practice: Software Tools and Applications. Imperial College Press, London, 2003.
【5】王东明，夏壁灿，李子明：计算机代数. 清华大学出版社, 北京, 2007年 (第二版).
【6】吴文俊：几何定理机器证明的基本原理 (初等几何部分). 科学出版社, 北京, 1984年.
【7】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.
【8】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.
【9】B. Xia and L. Yang: An algorithm for isolating the real solutions of semi-algebraic systems. J. Symb. Comput., 34: 461--477, 2002.
【10】B. Xia and T. Zhang: Algorithms for real root isolation based on interval arithmetic. Institute of Mathematics, Peking University, Research Report No. 107, 2003.
【11】B. Xia and T. Zhang: Real Solution Isolation Using Interval Arithmetic. Computers and Mathematics with Applications, 52: 853--860, 2006.
【12】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.
【13】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.
【14】L. Yang, X. Hou and Z. Zeng: A complete discrimination system for polynomials. Sci. China E 39(6) : 628--646, 1996.
【15】L. Yang and B. Xia: Automated Deduction in Geometry. In: Geometric Computation, 248--298. World Scientific, 2004.
【16】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.
【17】杨路，夏壁灿：不等式机器证明与自动发现. 科学出版社，2008年。
【18】杨路,张景中,侯晓荣：非线性代数方程组与定理机器证明. 上海科技教育出版社, 上海, 1996年.
【19】T. Zhang and B. Xia: A new method for real root isolation of univariate polynomials. In: Proc. the First International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS06), 85--91. Beijing, July 24-26, 2006.
