Geometry theorem proving by decomposition of quasi-algebraic sets: An application of the Ritt-Wu principle (Q1118424)

Wu used Ritt's chains to produce a canonical triangular basis of a polynomial ideal by applying a succession of some simple transformations. A canonical basis allows, in particular, to answer a question about empitness of a quasialgebraic set over an algebraically closed field. Some theorems from elementary geometry can be reformulated in the forms as follows: \(\forall z_ 1...\forall z_ n\) \((f_ 1(z_ 1,...,z_ n)=...=f_ s(z_ 1,...,z_ n)=0\) \(\Rightarrow\) \(g(z_ 1,...,z_ n)=0)\) for suitable polynomials \(f_ 1,...,f_ s\), g and thus one can prove them involving canonical bases. The paper contains examples of applying this scheme of proving to several known geometrical theorems.