computational geometry proofs; systems of equations

Robert Lewis lewis at
Mon Dec 6 15:03:23 PST 2004


I am interested in establishing geometrical results (not necessarily 
theorems) by computer algebra, specifically via the solution of 
multivariate polynomial equations.  I have used the Dixon resultant 
technique to do so, for example,

Lewis, Robert H. and Stephen Bridgett, "Conic Tangency Equations and 
Apollonius Problems in Biochemistry and Pharmacology," Mathematics and 
Computers in Simulation 61(2) (2003) p. 101-114. pdf version here:

Some computational geometric proofs using a different technique are on 
the web site

I wonder if anyone has tried (with such techniques) before to prove 
Ptolemy's theorem: For a quadalateral inscribed in a circle, let d1 and 
d2 be the (lengths of the) diagonals, d3 and d4 one pair of opposite 
sides, d5 and d6 the other. Then d1*d2 = d3*d4 + d5*d6.

I have done so by getting 9 equations in the 6 di and 8 other variables 
that represent the sine and cosine of various angles. The resultant is 
indeed d1*d2 - d3*d4 - d5*d6. It takes about 40 minutes cpu time to do 

I have also proved the converse: assuming d1*d2 - d3*d4 - d5*d6 = 0, 
the quadralateral is on a circle. This actually takes far less time, 
about five minutes.

Also, is there any information on similar three dimensional results?


Robert H. Lewis
Fordham University

The compgeom mailing lists: see
or send mail to compgeom-request at with the line:
send readme
Now archived at

More information about the Compgeom-announce mailing list