Mechanical decision for a class of integral inequalities

被引:0
作者
Lu Yang
WenSheng Yu
RuYi Yuan
机构
[1] East China Normal University,Shanghai Key Laboratory of Trustworthy Computing, Software Engineering Institute
[2] Chinese Academy of Sciences,The Key Laboratory of Complex Systems and Intelligence Science, Institute of Automation
[3] Chinese Academy of Sciences,Laboratory for Automated Reasoning and Programming, Chengdu Institute of Computer Applications
来源
Science China Information Sciences | 2010年 / 53卷
关键词
integral inequality; symmetric polynomial inequality; Timofte’s dimension-decreasing method; successive difference substitution; mechanical decision; inequality-proving package BOTTEMA;
D O I
暂无
中图分类号
学科分类号
摘要
A class of integral inequalities is transformed into homogeneous symmetric polynomial inequalities beyond Tarski model, where the number of elements of the polynomial, say n, is also a variable and the coefficients are functions of n. This is closely associated with some open problems formulated recently by Yang et al. Using Timofte’s dimension-decreasing method for symmetric polynomial inequalities, combined with the inequality-proving package BOTTEMA and a program of implementing the method known as successive difference substitution, we provide a procedure for deciding the nonnegativity of the corresponding polynomial inequality such that the original integral inequality is mechanically decidable; otherwise, a counterexample will be given. The effectiveness of the algorithm is illustrated by some more examples.
引用
收藏
页码:1800 / 1815
页数:15
相关论文
共 41 条
[11]  
Yang L.(1978)On the decision problem and the mechanization of theorem-proving in elementary geometry Sci China 21 150-172
[12]  
Yang L.(1990)The parallel numerical method of mechanical theorem proving Theo Comput Sci 74 253-271
[13]  
Yao Y.(1984)Cylindrical algebraic decomposition I: the basic algorithm SIAM J Comput 13 865-877
[14]  
Yao Y.(1984)Cylindrical algebraic decomposition II: an adjacency algorithm for the plane SIAM J Comput 13 878-889
[15]  
Wu W. T.(2001)Simple CAD construction and its applications J Symb Comput 31 521-547
[16]  
Zhang J. Z.(1991)Partial cylindrical algebraic decomposition for quantifier elimination J Symb Comput 12 299-328
[17]  
Yang L.(2007)A class of mechanically decidable problems beyond Tarski’s model Sci China Ser A-Math 50 1611-1620
[18]  
Deng M. K.(2001)A complete algorithm for automated discovering of a class of inequality-type theorems Sci China Ser F-Inf Sci 44 33-49
[19]  
Arnon D. S.(1996)A complete discrimination system for polynomials Sci China Ser E-Tech Sci 39 628-646
[20]  
Collins G. E.(2009)Optimal sublinear inequalities involving geometric and power means Math Bohem 134 133-149