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."
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)); |
![]() |
|
![]() |
(3.1.1) |
> |