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)&(H0) ===> 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_10 or h_20 or.....or h_r0} ===> 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