The simple idea behind them

Goal : to check the thesis follows from the hypotheses

AUTOMATIC PROVING

else,

to find complementary hypotheses for the thesis to follow from the given hypotheses

AUTOMATIC DISCOVERY

Algebraic method :

1) Translate the geometric construction and the thesis by means of a collection of equations and inequations:

H=0, T=0

2) Verify whether H=0 ===> T=0, by deciding if its negation

[Â(T=0)] &(H=0)

is the empty system (Nullstellensatz).

If empty, then H=0 ===> T=0

3) If the system is not empty, we must find other hypotheses H« such that either

(H=0)&(H«=0) ===> T=0

or

(H=0)&(H«­0) ===> T=0

To find complementary hypotheses H« is equivalent to

eliminate variables in one of the following systems....

¥H=0 &ÂT=0 (
non-degeneracy conditions )

because, obviously

H=0 & Â(H=0 &ÂT=0) ===> T=0

If H«=(h_1, h_2,..., h_r), then we obtain that

H=0 &{h_1­0 or h_2­0 or.....or h_r­0} ===> T=0

thus theorem will be true for any subset of these non-degeneracy conditions.

¥H=0 & T=0 (
discovery conditions )

because, obviously

H=0 & (H=0 & T=0) ===>T=0

If H«=(h_1, h_2,..., h_r), then we obtain that

H=0 &{h_1=0 and h_2=0 and.....and h_r=0} ===> T=0

so theorem could be true for any subset of these discovery conditions (but the more we consider, the better...).

Example 3 modified

Example 2 revisited

Example 3 revisited