A completion of hypotheses method for 3D-geometry. 3D-extensions of Ceva and Menelaus theorems

A Completion of Hyp otheses Metho d for 3D-Geometry. 3D-Extensions of Ceva and Menelaus Theorems 1 E. Roanes-Maas a , E. Roanes-Lozano  ; a a Dept. Algebra, Universidad Complutense de Madrid, Ediio \La Almudena", / Retor Royo Vil lanova s/n, 28040-Madrid, Spain Abstrat A metho d that automates hypotheses ompletion in 3D-Geometry is presented. It onsists of three pro esses: dening the geometri ob jets in the onguration; determining the hyp othesis onditions of the onguration (through a point-on-ob jet delaration method); and applying an algebrai automati theorem proving metho d to obtain and prove the suÆieny of omplementary hyp othesis onditions. To avoid as muh as possible the app earane of rational expressions, pro jetive o ordinates are used (although aÆne and Eulidean problems an also b e treated). A Maple implementation of the metho d has been used to extend to 3D lassi 2D geometri theorems like Ceva's and Menelaus'. Key words: 3D-Geometry, Simb oly Computation, Automati Theorem Proving 1. Brief Desription of the Metho d Hyp otheses ompletion was already treated by Reio and Velez [6℄. The metho d presented in this pap er automates hypotheses ompletion in 3DGeometry. Let us give a brief desription of its three pro esses. 1.1. Dening the Geometri Objets in the Conguration Among the geometri ob jets in a onguration, some an b e dened diretly and others are determined through geometri op erations (see Table 1). Other usual geometri ob jets inluded in the pakage (segment, midp oint, sphere, quadri,...) are omitted for the sake of spae. The desired onguration an be onstruted through the adequate onatenation of these elementary ommands. Note that in this Geome-  Corresp onding author Email addresses: roanesmat.um.es (E. RoanesMaas), eroanesmat.um.es (E. Roanes-Lozano). 1 Partially supp orted by the researh pro jet TIC-20001368-C03-03 (MCyT, Spain). try not only the rule-and-ompass global ly onstrutible ob jets an b e treated: those geometri ob jets suh that any of their p oints an b e onstruted with rule-and-ompass, an b e treated to o. Pro jetive o ordinates are used. Command intCoor allows to substitute o ordinates where rational expressions appear by the orresp onding integer quaternions. 1.2. Determining the hypothesis onditions of the onguration Hyp othesis onditions are delared as membership relations b etween p oints and higher dimension geometri ob jets. To delare P = [ p 0 ; p 1 ; p 2 ; p 3 ℄ as a p oint on the ob jet  (b eing the equations of  :  i ( x 0 ; x 1 ; x 2 ; x 3 ) = 0 ; i = 1 ; :::; n ) is equivalent to imp ose that the hypothesis onditions  i ( P 0 ; P 1 ; P 2 ; P 3 ) = 0 ; i = 1 ; :::; n are veried. Command pointOnObjet takes are of adding these p olynomials to a ertain list, denoted LRE L , where the hypothesis polynomials are stored, and to add the orresp onding variables to the list V AR . 20th EWCG Seville, Spain (2004) 20th Europ ean Workshop on Computational Geometry Ob jet Input Command Output initial p oint four pro jetive point list of 4 (free p oint) o ordinates parameters plane three non-ollinear plane equation of p oints the plane line two dierent line list of equations p oints of the line p oint on line AB two p oints ( A; B ) rateOnLine list of o ords. ( ! P B = r  ! P A ) and a real numb er r of p oint P plane/line parallel one linear ob jet parallel equation(s) of to a given plane/line and one p oint the plane/line plane/line p erp endiular one linear ob jet perpendiular equation(s) of to a given line/plane and one p oint the plane/line intersetion of two two already intersetion o ords. of p oint(s) ob jets (not dened ob jets or equation(s) of neessarily linear) linear ob jets or redued list of eqs. (in GB sense) Table 1 Geometri ob jets' denition 1.3. Obtaining and Proving the SuÆieny of Complementary Hypothesis Conditions In most onguration geometri problems, the thesis is (or an b e redued to) a P 2  memb ership ondition (where P is a point and  is a geometri ob jet) or to a geometri relation among geometri ob jets in the onguration. In b oth ases the thesis polynomial admits a  ( P ) form. In ase list LRE L is empty, to hek that the thesis holds is equivalent to hek that  vanishes in P (i.e., that  ( P ) = 0). Command isPlaed applied to the pair ( P ;  ) takes are of p erforming all the orresp onding omputations. In ase list LRE L is not empty, to hek that the thesis holds it is suÆient to hek that  an b e expressed as an algebrai linear ombination of the p olynomials in list LRE L , what an b e effetively omputed using Wu's tehniques. A brief desription of these automati proving tehniques an b e found in [1℄, meanwhile a detailed desription an be found, e.g., in [2,9℄. These tehniques were adapted to hyp otheses ompletion in [5℄ and to geometri loi determining in [7℄. The tehnique desrib ed in this pap er is essentially that of [7℄, but has b een adapted to the way hyp othesis and thesis onditions are usually delared. This pro ess basially onsists of two steps: { to triangularize system LRE L w.r.t. the variables in list V AR , to obtain system T RI P { to ompute, starting with  ( P ), the suessive pseudo-remainders of dividing by the p olynomials in T RI P w.r.t. the variables in V AR , until the last pseudo-remainder (p olynomial ! ) is obtained. That ! = 0 is a neessary ondition for the thesis to hold. Command newHypot of our pakage, applied to ( P ;  ), automatially omputes ! . But we would still have to hek that ! = 0 is a suÆient ondition for the thesis  ( P ) = 0 to hold. If a parametrization of ! = 0 an be obtained, then we substitute in  ( x 0 ; x 1 ; x 2 ; x 3 ) the x i by their orresp onding parametri expressions. If the resulting p olynomial vanishes, then ondition ! = 0 is also suÆient. Command isPlaed an take are of these omputations. If a parametrization of ! = 0 an't be obtained, then ! is b e added to list LRE L , and the new variable app earing in ! but not in list V AR , is added to list V AR . The same pro ess an b e applied now, Marh 25-26, 2004 Seville (Spain) and, if the last pseudo-remainder is 0, then ondition ! = 0 is also suÆient. Command autProve an take are of these omputations. 2. 3D-Extension of Ceva and Menelaus Theorems An appliation of the automati theorem proving metho d desrib ed ab ove is inluded as illustration afterwards. The goal is to determine onditions that make four p oints, lying on onseutive edge-lines of a tetrahedron, oplanary (see Figure 1). This problem was reently solved using syntheti tehniques by H. Davis [3℄. Fig. 1. Extending to 3D Ceva and Menelaus theorems We an assume that the verties are A (1 ; 0 ; 0 ; 0), B (1 ; 1 ; 0 ; 0), C (1 ;  1 ;  2 ; 0), D (1 ; Æ 1 ; Æ 2 ; Æ 3 ) without any lak of generality (these p oints an b e dened using ommand point ). Given m; n; p; q 2 R [ f1g , let M ; N ; P ; Q b e the p oints lying on the edge-lines AB ; B C; C D ; D A (resp etively), and satisfying ! M B = m  ! M A ; ! N C = n  ! N B ! P D = p  ! P C ; ! QA = q  ! QD (they an b e dened using ommand rateOnLine ). Then plane MNP an be dened (using ommand plane ). As detailed ab ove, applying ommand newHypot to the pair ( Q; M N P ), a neessary ondition for Q to lie on plane MNP (i.e., for M ; N ; P ; Q to b e oplanary):   2  Æ 3  (  1 + m  n  p  q ) = 0, is obtained. As A; B ; C; D are non-oplanary p oints, and onsequently,  2 6 = 0 6 = Æ 3 , what implies: m  n  p  q = 1. To verify that is a suÆient ondition, Q is partiularized for q = 1 = ( m  n  p ), and applying ommand isPlaed to the pair ( Q; M N P ), 0 is obtained, what onrms that Q b elongs to plane MNP . This leads to the following: Theorem 1 Points M ; N ; P ; Q , lying on the oriented onseutive edge-lines AB ; B C ; C D ; D A of tetrahedron AB C D (respetively), are oplanary, if and only if: ( M B =M A )  ( N C =N B )  ( P D =P C )  ( QA=QD ) = 1 Observe that the p oints M ; N ; P ; Q do lie on the onseutive oriented edge-lines AB ; B C ; C D ; D A , but they an lie outside the edge-segments, and therefore this result do esn't only generalizes Ceva theorem, but also Menelaus theorem. 3. Comparison with Other Metho ds As the automati theorem proving tehnique used in this work is based on Wu's algorithm, it is of a lower omputational omplexity than those tehniques based on the use of Groebner bases. Comparing this metho d with others based on Wu's tehniques, the main dierene is the way the geometri ob jets of the onguration are de- ned and the way the hyp otheses onditions are delared. In the method presented here the geometri ob jets and the hypotheses onditions are obtained in a natural way, following the geometri algorithm that generates the onguration, instead of translating into algebrai expressions the geometri relations that determine them (what is usually the ase). That happens, for instane, in Simson-SteinerGuzman theorem 3D-extension [4℄. The goal is to determine the onditions so that the pro jetions (in prexed diretions) of a p oint on the faes of a tetrahedron are oplanary. This problem was develop ed in [7℄, translating into algebrai expressions the geometri relations. Now it has b een develop ed using the method detailed in setion 1, in a more omfortable and faster way. 20th Europ ean Workshop on Computational Geometry Other advantage of the metho d prop osed in Se- tion 1 is the simple way in whih parameters and variables are distinguished (what is not straightforward in other approahes). With this metho d the parameters are the non-numeri o ordinates of the initial p oints (that are preserved along all subsequent alulations), meanwhile the variables are the o ordinates of the p oint-on-ob jet ob jets de- ned using pointOnObjet ommand. Another advantage of the metho d prop osed in Setion 1 is the p ossibility to develop the geometri algorithm of the onguration using a Dynami Geometry System, and to translate it to a Computer Algebra System syntax (interpreting it using the pakage onsidered here), as already done in 2D [8℄. We plan to implement it in the near future. 4. Conlusions The hypotheses ompletion in 3D-Geometry metho d desrib ed is onvenient and eÆient. It allows the user to obtain automatially the equations in the onguration, the hyp othesis onditions obtained diretly in the onguration and the omplementary hyp othesis onditions that have to b e added for the thesis ondition to hold. Referenes [1℄ D. Cox, J. Little and D. O'Shea, Ideals, Varieties, and Algorithms (Springer, New York, 1991). [2℄ S. C. Chou, Mehanial Geometry Theorem Proving (Reidel, Dordreht, 1988). [3℄ H. Davis, Menelaus and Ceva Theorems and its many appliations, http://hamiltonious.virtualave.negt/ essays/othe/nalpaper4.htm [4℄ M. de Guzman, An Extension of the WallaeSimson Theorem: Pro jeting in Arbitrary Diretions, Mathematial Monthly 106/6 (1999) 574{580. [5℄ D. Kapur and J.L. Mundy, Wu's metho d and its appliation to p ersp etive viewing, in: D. Kapur, J.L. Mundy, eds., Geometri Reasoning (MIT Press, Cambridge MA, 1989) 15{36. [6℄ T. Reio and M. P. Velez, Automati Disovery of Theorems in Elementary Geometry, Journal of Automated Reasoning 23 (1999) 63{82. [7℄ E. Roanes-Maas and E. Roanes-Lozano, Automati determination of geometri lo i, in: J. A. Camb ell and E. Roanes-Lozano, eds., Artiial Intel ligene and Symboli Computation . (Springer's Leture Notes in Artiial Intelligenge no. 1930, Berlin, 2000) 157{173. [8℄ E. Roanes-Lozano, E. Roanes-Maas and M. Villar, A Bridge Between Dynami Geometry and Computer Algebra, Mathematial and Computer Model ling 37/910 (2003) 1005{1028. [9℄ W. T. Wu, Mehanial Theorem Proving in Geometries (Springer-Verlag's Text and Monographs in Symb oli Computation, Wien, 1994).