Parametric CAD

¥ 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))

[Maple Metafile]

Vision, Pattern recognition

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

conjetural scene



[Maple Metafile]



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




[Maple Metafile]


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.



[Maple Metafile]

(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