zbMATH — the first resource for mathematics

A complete discrimination system for polynomials. (English) Zbl 0866.68104
Summary: 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 has never been given for polynomials with degrees greater than 4. The lack of efficient tools in this aspect extremely prevents oomputer implementations for Tarski’ s and other methods in automated theorem proving. To remedy this defect, a generic algorithm is proposed 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.

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68W30 Symbolic computation and algebraic computation
03B35 Mechanization of proofs and logical operations