关键词: 区间分析, 不等式, 自动证明

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.

Key words: interval analysis;inequality;automatic proving