[1]YANG Lu,YU Wensheng.Automated proving of some fundamental applied inequalities[J].CAAI Transactions on Intelligent Systems,2011,6(5):377-390.
Copy

Automated proving of some fundamental applied inequalities

CAAI Transactions on Intelligent Systems[ISSN 1673-4785/CN 23-1538/TP] Volume: 6 Number of periods: 2011 5 Page number: 377-390 Column: 学术论文—人工智能基础 Public date: 2011-10-30
Title:
Automated proving of some fundamental applied inequalities
Author(s):
YANG Lu;  YU Wensheng
Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China
Keywords:
fundamental applied inequalities; automated proving;  inequalityproving package BOTTEMA;  Tarski model
CLC:
TP181
DOI:
-
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.
Similar References:

Memo

-

Last Update: 2011-11-16

Copyright © CAAI Transactions on Intelligent Systems