Automated Reducible Geometric Theorem Proving and Discovery by Grobner Basis Method

In this paper, we investigate the problem that the conclusion is true on some components of the hypotheses for a geometric statement. In that case, the affine variety associated with the hypotheses is reducible. A polynomial vanishes on some but not all the components of a variety if and only if it is a zero divisor in a quotient ring with respect to the radical ideal defined by the variety. Based on this fact, we present an algorithm to decide if a geometric statement is generally true or generally true on components by the Grobner basis method. This method can also be used in geometric theorem discovery, which can give the complementary conditions such that the geometric statement becomes true or true on components. Some reducible geometric statements are given to illustrate our method.