InequalityProve及一个公开问题的求解

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

InequalityProve and the Solution to an Open Problem

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.