Example 1 

The teacher asks the student to prove that"The angle defined by a diameter of a circle from a point of the same circle is always a right angle."                       Image 

 


The student -turns on the pocket calculator, -introduces data (hypotheses and thesis), -pushes ENTER button and...-obtains a proof.
Hypothesis:
*circle of center (l/2,0), passing thru (0,0)
*(s,r) on circle: (s-l/2)^2+r^2-(l/2)^2=0

Thesis:
*(s,r)
^(s-l,r), ie. s(s-l)+r^2=0

Proof
Is    s(s-l)+r^2     in      Ideal((s-l/2)^2+r^2-(l/2)^2)) ?

In fact,  
            
s(s-l)+r^2 =  (s-l/2)^2+r^2-(l/2)^2               proof!!
   

 

> with(Groebner): G:=Basis({(s-l/2)^2+r^2-(l/2)^2},tdeg(s,l,r));
NormalForm(s*(s-l)+r^2, G, tdeg(s,l,r));
 

 

[`+`(`*`(`^`(s, 2)), `-`(`*`(s, `*`(l))), `*`(`^`(r, 2)))]
0 (3.1.1)
 

>