• 中国计算机学会会刊
  • 中国科技核心期刊
  • 中文核心期刊
论文

InequalityProve及一个公开问题的求解

展开
  • (电子科技大学自动化工程学院,四川 成都 611731)
邵俊伟(1984),男,湖北仙桃人,博士生,研究方向为实代数几何和稳定性理论。侯晓荣(1966),男,山西临县人,硕士,教授,研究方向为机器证明和控制理论。

收稿日期: 2010-05-25

  修回日期: 2010-09-03

  网络出版日期: 2011-06-25

基金资助

国家973计划资助项目(2004CB318000);国家自然科学基金资助项目(10571095)

InequalityProve and the Solution to an Open Problem

Expand
  • (School of Automation Engineering,University of
    Electronics Science and Technology of China,Chengdu 611731,China)

Received date: 2010-05-25

  Revised date: 2010-09-03

  Online published: 2011-06-25

摘要

传统的不等式自动证明方法主要依赖于符号计算,一般只能处理代数类型,或可最终转化为代数类型的不等式,而且效率会随着问题中变量个数的增加迅速降低。为克服这些局限性以满足众多实际问题的需要,并充分挖掘计算机在数值计算方面的能力,我们提出以区间分析为工具进行不等式的自动证明。该方法可以处理类型更为一般的不等式,只需对应的函数具有所需的高阶连续可微性质,并且该方法易于实现并行化。本文主要介绍这一方法在Maple系统上的实现,即InequalityProve,并以一个公开问题为例详细说明运用InequalityProve进行不等式证明的一般过程。

本文引用格式

邵俊伟,侯晓荣 . InequalityProve及一个公开问题的求解[J]. 计算机工程与科学, 2011 , 33(6) : 114 -117 . DOI: 10.3969/j.issn.1007130X.2011.

Abstract

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:139181.
[2]Wu WT. On a Finiteness Theorem about Problem Involving Inequalities[J]. Systems Science and Mathematical Science, 1994, 7(2):193200.
[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):357380.
[4]Yang L, Hou X R, Xia B C. A Complete Algorithm for Automated Discovering of a Class of InequalityType Theorems[J]. Science in China F, 2001, 44:3349.
[5]杨路, 夏时洪. 一类构造性几何不等式的机器证明[J]. 计算机学报, 2003, 26(7):769778.
[6]杨路. 差分代换与不等式机器证明[J]. 广州大学学报(自然科学版), 2006, 5(2):17.
[7]杨路, 夏壁灿. 不等式机器证明与自动发现[M]. 北京:科学出版社, 2008.
[8]侯晓荣,邵俊伟. 基于区间分析的不等式自动证明[J].系统科学与数学,2010(10):13511358.
[9]Moore R E, Kearfott R B, Cloud M J. Introduction to Interval Analysis[M]. SIAM, 2009.
[10]匡继昌.常用不等式[M]. 第三版.济南: 山东科学技术出版社, 2004.

文章导航

/