×

zbMATH — the first resource for mathematics

Towards mechanical solution of the Kahan ellipse problem. I. (English) Zbl 0553.68031
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.)