摘要
１Ａｌｇｅｂｒａｉｃａｐｐｒｏａｃｈｅｓ：ａｃｈｉｅｖｅｍｅｎｔｓａｎｄｄｉｆｉｃｕｌｔｉｅｓＷｅｈａｖｅｒｅａｓｏｎｔｏｂｅｌｉｅｖｅｔｈａｔｃｏｍｐｕｔｅｒｗｉｌｐｌａｙａｍｕｃｈｍｏｒｅｉｍｐｏｒｔａｎｔｒｏｌｅｉｎｒｅａｓｏｎｉｎｇｓｃｉｅ...
Automated inequality proving has been a difficult topic in the area of automated reasoning for many years. The concerning algorithms depend on real algebra and real geometry, and the computational complexity increases very quickly with the dimension, i.e. 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 lowest. Based on this algorithm, a generic program called “ BOTTEMA” was implemented on a PC computer. About 500 algebraic and geometric inequalities including more than 100 open problems have been verified in this way. The total CPU time spent for proving 120 basic inequalities from Bottema’s monograph, “Geometric Inequalities” on a Pentium/200, was 20 odd seconds only.
