<-上一篇/Previous Article 下一篇/Next Article->

[1]杨路,郁文生.常用基本不等式的机器证明[J].智能系统学报,2011,6(5):377-390.
　YANG Lu,YU Wensheng.Automated proving of some fundamental applied inequalities[J].CAAI Transactions on Intelligent Systems,2011,6(5):377-390.

点击复制

常用基本不等式的机器证明

PDF下载 HTML

《智能系统学报》[ISSN 1673-4785/CN 23-1538/TP] 卷: 6 期数: 2011年第5期页码: 377-390 栏目: 学术论文—人工智能基础出版日期: 2011-10-30

Title:: Automated proving of some fundamental applied inequalities

文章编号:: 1673-4785(2011)05-0377-14

作者:: 杨路,郁文生; 华东师范大学上海高可信计算重点实验室，上海 200062

Author(s):: YANG Lu， YU Wensheng; Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China

关键词:: 基本不等式; 机器证明; 不等式证明软件BOTTEMA; Tarski模型

Keywords:: fundamental applied inequalities; automated proving; inequalityproving package BOTTEMA; Tarski model

分类号:: TP181

文献标志码:: A

摘要:: 不等式机器证明问题是智能系统领域的难点和热点问题.借助不等式证明软件BOTTEMA，对若干常用的基本不等式成功地实现了机器证明，包括算术、几何与调和平均不等式、排序不等式、Chebyshev不等式、Bernoulli不等式、三角形不等式及Jensen不等式等.所论不等式含有的变元个数是一个不确定的变量，属于Tarski模型外的不等式类型.机器证明得出的结论有时可能是已知结果的推广，其方法本身对同类不等式有示范性，更多的例子表明了该算法和软件的有效性.

Abstract:: The automated proving of inequalities is always a difficult and hot topic in the field of intelligence systems. In this paper, by means of an inequalityproving package called BOTTEMA, the automated proving for some fundamental applied inequalities is successfully implemented. These inequalities include the arithmeticgeometricharmonic inequality, arrangement inequality, Chebyshev inequality, Bernoulli inequality, triangle inequality, and Jensen inequality, beyond the Tarski model, where the number of variables of the inequality is also a variable. The conclusions obtained from automated proving sometimes may extend the known results; and the method would be of use for analogous types of inequalities. The effectiveness of the algorithm and package is illustrated by some more examples. 

参考文献/References:: ［1］杨路,夏壁灿.不等式机器证明与自动发现:数学机械化丛书［M］.北京：科学出版社, 2008.
［2］TARSKI A. A decision method for elementary algebra and geometry［M］. Berkeley, USA: The University of California Press, 1951.
［3］吴文俊.初等几何判定问题与机械化证明［J］.中国科学：数学, 1977, 20(6): 507516.
WU Wenjun. On the decision problem and mechanization of theoremproving in elementarygeometry［J］. Science China Mathemation, 1977, 20(6): 507516.
［4］吴文俊.几何定理机器证明的基本原理［M］.北京：科学出版社, 1984.
［5］吴文俊. 数学机械化:数学机械化丛书［M］.北京：科学出版社, 2003.
［6］杨路,张景中,侯晓荣.非线性代数方程组与机器证明:非线性科学丛书［M］.上海：上海科学教育出版社, 1996.
［7］ARNON D S, COLLINS G E, MCCALLUM S. Cylindrical algebraic decomposition I: the basic algorithm［J］. SIAM Journal on Computing, 1984, 13(4): 865877.
［8］ARNON D S, COLLINS G E, MCCALLUM S. Cylindrical algebraic decomposition II: an adjacency algorithm for the plane［J］. SIAM Journal on Computing, 1984, 13(4): 878889.
［9］BROWN C W. Simple CAD construction and its applications［J］. Journal of Symbolic Computation, 2001, 31(5): 521547.
［10］COLLINS G E. Quantifier elimination for real closed fields by cylindrical algebraic decomposition［C］//Automata Theory and Formal Languages. Kaiserslautern, Germany, 1975: 134183.
［11］COLLINS G E, HONG H. Partial cylindrical algebraic decomposition for quantifier elimination［J］. Journal of Symbolic Computation, 1991, 12(3): 299328.
［12］CHOU S C. Mechanical geometry theorem proving［M］. Dordrecht, Holland: D. Reidel Publishing Company, 1988.
［13］CHOU S C, ZHANG J Z, GAO X S. Machine proofs in geometry: automated production of readable proofs for geometry theorems［M］. Singapore: World Scientific, 1994.
［14］杨路,侯晓荣,曾振柄.多项式的完全判别系统［J］.中国科学:E辑, 1996, 26 (5): 424441.
YANG Lu, HOU Xiaorong, ZENG Zhenbing. A complete discrimination system for polynomials［J］. Science in China: Series E, 1996, 26(5): 424441.
［15］杨路.不等式机器证明的降维算法与通用程序［J］.高技术通讯, 1998, 8(7): 2025.
YANG Lu. A dimensiondecreasing algorithm with generic program for automated inequalities proving［J］. High Technology Letters, 1998, 8(7): 2025.
［16］YANG Lu. Practical automated reasoning on inequalities: generic programs for inequality proving and discovering［C］//Proceedings of the Third Asian Technology Conference in Mathematics. Tsukuba, Japan, 1998: 2435.
［17］YANG Lu. Recent advances in automated theorem proving on inequalities［J］. Journal of Computer Science and Technology, 1999, 14(5): 434446.
［18］杨路,夏时洪.一类构造性几何不等式的机器证明［J］.计算机学报, 2003, 26(7): 769778.
YANG Lu, XIA Shihong. Automated proving for a class of constructive geometric inequalities［J］. Chinese Journal of Computer, 2003, 26(7): 769778.
［19］YANG Lu, ZHANG Ju. A practical program of automated proving for a class of geometric inequalities［C］//The Third International Workshop on Automated Deduction in Geometry. London, UK: SpringerVerlag, 2001: 4157.
［20］杨路,侯晓荣,夏壁灿.自动发现不等式型定理的一个完备算法［J］.中国科学:E辑, 2001, 31(3): 424441.
YANG Lu, HOU Xiaorong, XIA Bican. A complete algorithm for automated discovering of a class of inequalitytype theorems［J］. Science in China: Series E, 2001, 31(3): 424441.
［21］DOLZMANN A, STURM T. REDLOG: computer algebra meets computer logic［J］. ACM SIGSAM Bulletin, 1997, 31(2): 29.
［22］BOTTEMA O, DORDEVIC R Z, JANIC R R, et al. Geometric inequlities［M］. Groningen, The Netherlands: WoltersNoordhoff Publishing, 1969.
［23］GERHOLD S, KAUERS M. A procedure for proving special function inequalities involving a discrete parameter［C］//Proceedings of the 2005 International Symposium on Symbolic and Algebraic Computation. New York, USA: ACM Press, 2005: 156162.
［24］GERHOLD S, KAUERS M. A computer proof of Turán inequality［J］. Journal of Inequalities in Pure and Applied Mathematics, 2006, 7(2): Article 42.
［25］KAUERS M. Computer proofs for polynomials identities in arbitrary many variables［C］//Proceedings of the 2004 International Smposium on Symbolic and Agebraic Cmputation. New York, USA: ACM Press, 2004: 199204.
［26］杨路,姚勇,冯勇.Tarski模型外的一类机器可判定问题［J］.中国科学:A辑, 2007, 37 (5): 513522.
YANG Lu, YAO Yong, FENG Yong. A class of machine determination problem besides the Tarski model［J］. Science China: Series A, 2007, 37(5): 513522.
［27］YANG Lu, YU Wensheng, YUAN Ruyi. Mechanical decision for a class of intergral inequalities［J］. Science China Information Sciences, 2010, 53(9): 18001815.
［28］HARDY G H, LITTLEWOOD J E, POLYA G. Inequalities［M］. Cambridge, UK: Cambridge University Press, 1988.
［29］MARSHALL A W, OLKIN I. Inequalities: theory of majorization and its applications［M］. New York, USA: Academic Press, 1979.
［30］MITRINOVIC D S. Elementary inequlities［M］. Groningon, The Netherlands: P. Noordhoff Ltd., 1964.
［31］MITRINOVIC D S, VASIC P M. Analytic inequalities［M］.Berlin, Germany： Springer， 1970.
［32］张福春,李姿霖.不等式之基本解题方法［J］.数学传播, 2007, 31(2): 3861.
ZHANG Fuchun, LI Zilin. The basic problemsolving methods for inequality［J］. Mathematical Communication, 2007, 31(2): 3861.
［33］匡继昌.常用不等式［M］.4版.济南：山东科学技术出版社, 2010.
［34］ACZEL J. Some general methods in the theory of functional equations in one variable: new applications of functional equations［J］. Uspekhi Matematicheskikh Nauk, 1956, 11(3): 368.
［35］ACZEL J, VARGA O. Bemerkung zur CayleyKleinschen Massbestimmung［J］. Punl Math, 1955, 4: 315.
［36］NANJUNDIAH T S. Problem 10347［J］. The American Mathematical Monthly, 1993, 100(10): 951952.
［37］BEESACK P R. On certain discrete inequalities involving partial sums［J］. Canadian Journal of Mathematics, 1969, 21: 222234.

备注/Memo

收稿日期： 2011-04-13.
基金项目：国家自然科学基金资助项目(61070048,60874010);国家自然科学基金委员会创新研究群体科学基金资助项目(61021004);国家“863”计划资助项目(2011AA010101)；国家“973”计划资助项目(2011CB302802,2011CB302400)；上海市重点学科建设资助项目(B412)；上海市教育委员会科研创新资助项目(11ZZ37). 
通信作者：郁文生.E-mail:wsyu@sei.ecnu.edu.cn.
作者简介：
杨路，男，1936年生，教授，博士生导师，主要研究方向为定理机器证明、数学机械化与推理自动化、计算代数几何特别是计算实代数几何及其在信息技术领域的应用等.
郁文生，男，1967年生，教授，博士生导师，博士,主要研究方向为鲁棒控制、泛函微分方程理论、符号计算和实代数理论及应用、系统全局优化、数学机械化与推理自动化及其在信息技术领域的应用等.

更新日期/Last Update: 2011-11-16

常用基本不等式的机器证明 PDF下载HTML

备注/Memo

常用基本不等式的机器证明

PDF下载 HTML