Automated proof of mixed trigonometric-polynomial inequalities. (November 2020)

• Record Type: Journal Article
• Authors: Chen, Shiping; Liu, Zhong
• Is Part Of: Journal of symbolic computation. Volume 101(2020)
• Page Start: 318
• Page End: 329
• Publication Date: 2020-11
• Subjects: Mixed trigonometric-polynomial -- Taylor substitution -- Readable proof; Mathematics -- Data processing -- Periodicals; Numerical analysis -- Data processing -- Periodicals; Automatic programming (Computer science) -- Periodicals; Mathématiques -- Informatique -- Périodiques; Analyse numérique -- Informatique -- Périodiques; Programmation automatique -- Périodiques; Automatic programming (Computer science); Mathematics -- Data processing; Numerical analysis -- Data processing; Periodicals; Electronic journals; 510.285
• DOI: 10.1016/j.jsc.2019.10.002
• Languages: English
• ISSNs: 0747-7171

Abstract

Abstract: This paper presents an algorithm for automated proof of inequalities involving a certain class of generalized polynomials where the monomials contain one variable and trigonometric functions applied to the same variable. Through Taylor Expansion, the proving of the target inequality is reduced to the verification of a series of polynomial inequalities with only one variable, and then completed by algebraic inequality-proving package such as BOTTEMA. The algorithm is complete and experiments show that it is very effective for trigonometric-polynomial inequalities, furthermore, the procedure is 'readable'.