Recent advances in automated theorem proving on inequalities |
| |
Authors: | Lu Yang |
| |
Affiliation: | (1) Chengdu Institute of Computer Applications, Chinese Academy of Sciences, 610041 Chengdu, P.R. China |
| |
Abstract: | 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. |
| |
Keywords: | inequality with radicals rationalization dichotomous search |
本文献已被 CNKI 维普 万方数据 SpringerLink 等数据库收录! |
| 点击此处可从《计算机科学技术学报》浏览原始摘要信息 |
|
点击此处可从《计算机科学技术学报》下载全文 |
|