Computer Engineering & Science >
InequalityProve and the Solution to an Open Problem
Received date: 2010-05-25
Revised date: 2010-09-03
Online published: 2011-06-25
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.
SHAO Junwei,HOU Xiaorong . InequalityProve and the Solution to an Open Problem[J]. Computer Engineering & Science, 2011 , 33(6) : 114 -117 . DOI: 10.3969/j.issn.1007130X.2011.
［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.
/
| 〈 |
|
〉 |