**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_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 **