Towards mechanical solution of the Kahan ellipse problem I

Abstract

Tarski (1948) gave a quantifier elimination procedure for elementary algebra and geometry which, when implemented, was found to be impractical. Collins (1975) gave a different and far more efficient algorithm, which has revived interest in the feasibility of quantifier elimination as a means of solving nontrivial problems in elementary algebra and geometry. Collins' algorithm has recently been implemented (1981). Experience so far obtained with the software indicates that, while some worthwhile problems can now be solved, it is desirable to find methods for improving performance. In this paper we report on several such methods, that we have developed in the course of applying the Collins algorithm to the Kahan ellipse problem. These methods have yielded substantial performance improvements; in fact, they have made feasible computations relating to the Kahan problem that initially could not be carried out at all in our computing environment. We are pursuing the further development of these techniques, with the goal of eventually producing a solution to the Kahan problem using the Collins algorithm.