Towards mechanical solution of the Kahan ellipse problem. I. (English) Zbl 0553.68031

Arnon, Dennis S.; Smith, Scott F.

Computer algebra, EUROCAL ’83, Proc. Conf., London 1983, Lect. Notes Comput. Sci. 162, 36-44 (1983).

[For the entire collection see Zbl 0532.00010.]
The authors present means for a speed-up of the Collins decision algorithm for the theory of the real closed fields [G. E. Collins, Lect. Notes Comput. Sci. 33, 134-183 (1975; Zbl 0318.02051)]. The Collins algorithm may also be applied to solve the Kahan ellipse problem, i.e., to find a, b, c, d for which \((\forall x)(\forall y)((x-c)^ 2/a^ 2+(y-d)^ 2/b^ 2=1\to y^ 2+x^ 2<1)\) holds, but proved to be inefficient in this case. Thus, the authors give a survey of the Collins method and discuss the necessity for a preprocessing of the formulas. Such a preprocessing may consist in the application of a simple rule in predicate logic, namely: \((\forall u)(\forall v)(F(u)=G(v)\to \phi (u,G(v)))\) implies \((\forall u)((\exists v)F(u)=G(v)\to \phi (u,F(u))).\) It is shown, that for the case \(d=0\) the Collins algorithm, applied to Kahan’s ellipse problem, may be improved by this rule. Finally the authors propose a priori restrictions on free variables as a mean of improved by this rule. Finally the authors propose a priori restrictions on free variables as a mean of improvement.

Reviewer: A.Leitsch

MSC:

68W30	Symbolic computation and algebraic computation
68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)
03C10	Quantifier elimination, model completeness, and related topics
03B35	Mechanization of proofs and logical operations
12L12	Model theory of fields
12D15	Fields related with sums of squares (formally real fields, Pythagorean fields, etc.)

Keywords:

Collins decision algorithm; real closed fields; Kahan ellipse problem

Citations:

Zbl 0532.00010; Zbl 0318.02051