Recent Advances in Automated Theorem Proving on Inequalities

摘要

Automated theorem proving on inequalities is always considered as a difficult topic in the area of automated reasoning. The relevant algorithms depend fundamentally on real algebra and real geometry, and the computational complexity increases very quickly with the dimension, that is, the number of parameters. Some well-known algorithms are complete theoretically but inefficient in practice, which cannot verify non-trivial propositions in batches. A dimension-decreasing algorithm presented here can treat radicals efficiently and make the dimensions the lowest. Based upon this algorithm, a generic program called "BOTTEMA" was implemented on a personal computer. More than 1000 algebraic and geometric inequalities includ- ing hundreds of open problems have been verified in this way. This makes it possible to check a finite many inequalities instead of solving a globa-optimization problem.