摘要
Automated theorem proving on inequalities is always considered asa difficult topic in the area of automated reasoning. The relevallt algorithms dependfundamentally on real algebra and real geometry, and the computational complexityincreases very quickly with the dimension, that is, the number of parameters. Somewell-known algorithms are complete theoretically but inefficient in practice, whichcannot verify non-trivial propositions in batches. A dimension- decreasing algorit hmpresellted here can treat radicals efficiently and make the dimensions the lowest.Based upon this algorithm, a generic program called 'BOTTEMA' was implementedon 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 possibleto check a finite many inequalities instead of solving a globaloptimization problem.
Automated theorem proving on inequalities is always considered asa difficult topic in the area of automated reasoning. The relevallt algorithms dependfundamentally on real algebra and real geometry, and the computational complexityincreases very quickly with the dimension, that is, the number of parameters. Somewell-known algorithms are complete theoretically but inefficient in practice, whichcannot verify non-trivial propositions in batches. A dimension- decreasing algorit hmpresellted here can treat radicals efficiently and make the dimensions the lowest.Based upon this algorithm, a generic program called 'BOTTEMA' was implementedon 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 possibleto check a finite many inequalities instead of solving a globaloptimization problem.
