InequalityProve及一个公开问题的求解
收稿日期: 2010-05-25
修回日期: 2010-09-03
网络出版日期: 2011-06-25
基金资助
国家973计划资助项目(2004CB318000);国家自然科学基金资助项目(10571095)
InequalityProve and the Solution to an Open Problem
Received date: 2010-05-25
Revised date: 2010-09-03
Online published: 2011-06-25
邵俊伟,侯晓荣 . InequalityProve及一个公开问题的求解[J]. 计算机工程与科学, 2011 , 33(6) : 114 -117 . DOI: 10.3969/j.issn.1007130X.2011.
Traditional methods of automatic inequality proving mainly make use of symbolic computation, and generally deal with algebraic inequalities or inequalities that can be ultimately converted to algebraic types. The efficiencies of these methods decrease rapidly as variable numbers grow. In order to meet the needs in practice, and make full use of the numerical computation power of computers, we propose a method of proving inequalities automatically based on interval analysis. This method can be applied to more general types of inequalities, which only need to be continuously differentiable to the required orders, moreover, it can be easily parallelized. InequalityProve is the implementation of the automatic inequality proving method based on interval analysis on the Maple system. The general steps of automatically proving inequalities using InequalityProve are introduced, and detailed procedures are illustrated through solving an open problem.
[1]Chou S C, Gao X S, Arnon D S. On the Mechanical Proof of Geometry Theorems Involving Inequalities[J]. Advances in Computing Research, 1992, 6:139181.
[2]Wu WT. On a Finiteness Theorem about Problem Involving Inequalities[J]. Systems Science and Mathematical Science, 1994, 7(2):193200.
[3]Dolzmann A, Sturm T, Weispfenning V. A New Approach for Automatic Theorem Proving in Real Geometry[J]. Journal of Automated Reasoning, 1998, 21(3):357380.
[4]Yang L, Hou X R, Xia B C. A Complete Algorithm for Automated Discovering of a Class of InequalityType Theorems[J]. Science in China F, 2001, 44:3349.
[5]杨路, 夏时洪. 一类构造性几何不等式的机器证明[J]. 计算机学报, 2003, 26(7):769778.
[6]杨路. 差分代换与不等式机器证明[J]. 广州大学学报(自然科学版), 2006, 5(2):17.
[7]杨路, 夏壁灿. 不等式机器证明与自动发现[M]. 北京:科学出版社, 2008.
[8]侯晓荣,邵俊伟. 基于区间分析的不等式自动证明[J].系统科学与数学,2010(10):13511358.
[9]Moore R E, Kearfott R B, Cloud M J. Introduction to Interval Analysis[M]. SIAM, 2009.
[10]匡继昌.常用不等式[M]. 第三版.济南: 山东科学技术出版社, 2004.
/
| 〈 |
|
〉 |