¥ Parametric Computer Aided Geometric Design,

Automatic Geometric Reasoning

Hoffman, Kapur, Chou, Wu, Wang, Buchberger, Joan-Arinyo

General Electric

Finding solutions to an initial sketch with restrictions
(distance, tangency, perpendicularity, incidence, collinearity, etc..)

distance(a,b)=d1
distance(b,c)=d2
distance(a,d)=d3
tangent(segment (a,b), circle(Q))
tangent(segment (b,c), circle(Q))
on(d,circle(Q))
on(c,circle(Q))

Vision, Pattern recognition

-consistency: given two images, to determine if they come from one

conjetural scene

-obtaining restrictions to the scene as imposed by image properties.

Hypotheses or Construction :

¥polynomial equations,
¥inequations

eg. relation between given and projected points, sketch...

Thesis or Conclusion :

¥eg. paralellism,
¥existence of solution,
¥perpendicularity condition, etc..

Symbolic coefficients: integers, integers+parameters

¥Checking if thesis follows from hypotheses:

Automatic proving

¥Searching for complementary hypotheses for the thesis to become true

AUTOMATIC DISCOVERY

¥
Example (with CoCoA):

For a given triangle, we claim the circumcenter lies on one side.

(x,y) circumcenter

Theorem is false:

NormalForm(1,Ideal(x^2+y^2-(x-e)^2-y^2,x^2+y^2-(x-a)^2-(y-b)^2, yt-1))

1;

Theorem does not provide degeneracy complementary hypotheses:

Elim(t..y,Ideal(x^2+y^2-(x-e)^2-y^2,x^2+y^2-(x-a)^2-(y-b)^2, yt-1))

Ideal( 0 );

Theorem provides complementary restrictions

Elim(t..y,Ideal(x^2+y^2-(x-e)^2-y^2,x^2+y^2-(x-a)^2-(y-b)^2, y))

Ideal( a^2e + b^2e - ae^2 );

We add this new hypothesis and look for degeneracy conditions in the new situation:

Elim(t..y,Ideal(x^2+y^2-(x-e)^2-y^2,x^2+y^2-(x-a)^2-(y-b)^2, a^2e+b^2e-ae^2, yt-1))

Ideal( a^2e - ae^2 ,
be );

Hence, if result holds then:

a^2e+b^2e-ae^2=0 and
be­0 or a^2e - ae^2­0

In particular,

be­0, a^2+b^2-ae=0,

ie. rectangular triangle.

NormalForm(1,Ideal(x^2+y^2-(x-e)^2-y^2,x^2+y^2-(x-a)^2-(y-b)^2, a^2e+b^2e-ae^2, beh-1, yt-1))

0