[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.
点击复制

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

参考文献/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
Copyright © 《 智能系统学报》 编辑部
地址:(150001)黑龙江省哈尔滨市南岗区南通大街145-1号楼 电话:0451- 82534001、82518134 邮箱:tis@vip.sina.com