A complete algorithm for automated discovering of a class of inequality-type theorems. (English) Zbl 1125.68406

Summary: Making use of the discriminant sequence for polynomials, WR algorithm, Wu’s elimination and a partial cylindrical algebraic decomposition, we present here a practical algorithm for automated inequality discovering which can discover new inequalities automatically without requiring to put forward any conjectures beforehand. That is complete for an extensive class of inequality-type theorems. Also this algorithm is applied to the classification of the real physical solutions of geometric constraint problems. Many inequalities with various backgrounds have been discovered or rediscovered by our program, DISCOVERER, which implements the algorithm in Maple.


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
03C10 Quantifier elimination, model completeness, and related topics


Full Text: DOI


[1] Folke, E., Which triangles are plane sections of regular tetrahedra? American Mathematical Monthly, Oct., 1994, 788. · Zbl 0831.51013
[2] Guy, R. K., Nowakowski, R. J., Monthly Unsolved Problems, 1969–1997, American Mathematical Monthly, Dec., 1997, 967.
[3] Yang, L., Zhang, J. Z., Hou, X. R., An efficient decomposition algorithm for geometry theorem proving without factorization, in Proceedings of Asian Symposium on Computer Mathematics 1995 (eds. Shi, H., Kobayashi, H.), Scientists Incorporated Japan, 1995, 33–41.
[4] Yang, L., Zhang, J. Z., Hou, X. R., Nonlinear Algebraic Equation System and Automated Theorem Proving (in Chinese), Shanghai: Shanghai Scientific and Technological Education Publishing House, 1996.
[5] Yang, L., Xia, B. C., Explicit criterion to determine the number of positive roots of a polynomial, MM Research Preprints, 1997, (15): 134–145.
[6] Liang, S. X., Zhang, J. Z., A complete discrimination system for polynomials with complex coefficients and its automatic generation, Science in China, Series E, 1999, 42(2): 113. · Zbl 0949.12002
[7] Yang, L., Recent advances on determining the number of real roots of parametric polynomials, Journal of Symbolic Computation, 1999, 28: 225. · Zbl 0957.65041
[8] Zhu, S. M., Wu, X. M., Computer application to ordinary differential equations and soliton, Mathematical Technology for 21st Century (eds. Yang, L., Liang, S. X.) (in Chinese), Guangzhou: Guangdong Economy Publishing House, 1999, 32–39.
[9] Wang, L., Yu, W. S., Complete characterization of strictly positive real regions and robust strictly positive real synthesis method, Science in China, Series E, 2000, 43(1): 97. · Zbl 0966.93042
[10] Yang, L., Hou, X. R., Zeng, Z. B., A complete discrimination system for polynomials, Science in China, Series E, 1996, 39(6): 628. · Zbl 0866.68104
[11] Chen, M., Generalization of discrimination system for polynomials and its applications, Ph. D Dissertation, Sichuan Union University, 1998.
[12] González-Vega, L., Lombardi, H., Recio, T. et al., Sturm-Habicht sequence, in Proc. of ISSAC’89, New York: ACM Press, 1989, 136–146.
[13] Arnon, D. S., Collins, G. E., McCallum, S., Cylindrical algebraic decomposition I: The basic algorithm, SIAM J. Comput., 1984, 13(4): 865. · Zbl 0562.14001
[14] Arnon, D. S., Collins, G. E., McCallum, S., Cylindrical algebraic decomposition II: An adjacency algorithm for the Plane, SIAM J. Comput., 1984, 13(4): 878. · Zbl 0562.14001
[15] Winkler, F., Polynomial Algorithms in Computer Algebra, Wien: Springer-Verlag, 1996. · Zbl 0853.12003
[16] Wu, W. T., On the decision problem and the mechanization of theorem-proving in elementary geometry, Sci. Sinica, 1978, 21: 159. · Zbl 0376.68057
[17] Wu, W. T., Mechanical Theorem Proving in Geometries: Basic Principles, Berlin: Springer-Verlag, 1994. · Zbl 0831.03003
[18] Gao, X. S., Cheng, H. F., On the solution classification of the ”P3P” problem, in Proc. of ASCM’98 (ed. Li, Z.), Lanzhou: Lanzhou University Press, 1998, 185–200.
[19] Yang, L., A simplified algorithm for solution classification of the perspective-three-point problem, MM Research Preprints, Beijing, 1998, 135.
[20] Mitrinovic, D. S., Pecaric, J. E., Volenec, V., Recent Advances in Geometric Inequalities, Amsterdam: Kluwer Academic Publishers, 1989.
[21] Briggs, W. E., Zeros and factors of polynomials with positive coefficients and protein-ligand binding, Rocky Mountain Journal of Mathematics, 1985, 15(1): 75. · Zbl 0575.12018
[22] Wyman, J., The Binding potential, A neglected linkage concept, J. Mol. Biol., 1965, 11: 631.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.