Lu Yang, Xiao-Rong Hou and Zhen-Bing Zeng
Laboratory for Automated Reasoning and Programming
Chengdu Institute of Computer Applications, Academia Sinica
610041 Chengdu, P. R. China
Given a polynomial with symbolic/literal coefficients, a complete
discrimination system is a set of explicit expressions in terms of
the coefficients, which is sufficient for determining the numbers and
multiplicities of the real and imaginary roots. Though it is of great
significance, such a criterion for root-classification had never been
given for polynomials with degrees greater than 4. The lack of efficient
tools in this aspect extremely prevents computer implementations for
Tarski's method and other ones in Automated Theorem Proving. To remedy
this defect, the authors propose a generic algorithm to produce a complete
discrimination system for a polynomial with any degree. This result has
extensive applications in various fields, and its efficiency was
demonstrated by computer implementations.