Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Automated Deduction in Geometry

ADG 2006: Automated Deduction in Geometry pp 171–188Cite as

A Maple Package for Automatic Theorem Proving and Discovery in 3D-Geometry

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 4869))

Abstract

A package for investigating problems about configuration theorems in 3D-geometry and performing mechanical theorem proving and discovery is presented. It includes the preparation of the problem, consisting of three processes: defining the geometric objects in the configuration; determining the hypothesis conditions through a point-on-object declaration method; and fixing the thesis conditions. After this preparation, methods based both on Groebner Bases and Wu’s method can be applied to prove thesis conditions or to complete hypothesis conditions. Homogeneous coordinates are used in order to treat projective problems (although affine and Euclidean problems can also be treated). A Maple implementation of the method has been developed. It has been used to extend to 3D some classic 2D theorems.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Roanes-Macías, E., Roanes-Lozano, E.: Nuevas Tecnologías en Geometría. Editorial Complutense, Madrid (1994)

    Google Scholar 

  2. Roanes-Lozano, E., Roanes-Macías, E.: Automatic Theorem Proving in Elementary Geometry with DERIVE 3. The Intl. DERIVE J. 3(2), 67–82 (1996)

    Google Scholar 

  3. Roanes-Lozano, E., Roanes-Macías, E.: Mechanical Theorem Proving in Geometry with DERIVE-3. In: Bärzel, B. (ed.) Teaching Mathematics with DERIVE and the TI-92. ZKL-Texte Nr.2, Bonn, pp. 404–419 (1996)

    Google Scholar 

  4. http://education.ti.com/educationportal/sites/US/productDetail/us_cabri_geometry.html

  5. http://www.cinderella.de

  6. Kortenkamp, U.: Foundations of Dynamic Geometry (Ph.D. Thesis). Swiss Fed. Inst. Tech. Zurich, Zurich (1999)

    Google Scholar 

  7. http://www.acailab.com/english/mathxp.htm

  8. Fu, H., Zeng, Z.: A New Dynamic Geometry Software with a Prover and a Solver. In: Proceedings of VisiT-me’2002. Vienna International Symposium on Integrating Technology into Mathematics Teaching, BK-Teachware, Hagenberg, Austria (2002) (CD-ROM)

    Google Scholar 

  9. http://www-calfor.lip6.fr/~wang/GEOTHER/

  10. Wang, D.: GEOTHER 1.1: Handling and Proving Geometric Theorems Automatically. In: Winkler, F. (ed.) ADG 2002. LNCS (LNAI), vol. 2930, Springer, Heidelberg (2004)

    Google Scholar 

  11. Wang, D.: Epsilon: Software Tool for Polynomial Elimination and Descomposition, http://www-calfor.lip6.fr/~wang/epsilon

  12. Botana, F., Valcarce, J.L.: A dynamic-symbolic interface for geometric theorem discovery. Computers and Education 38(1-3), 21–35 (2002)

    Article  Google Scholar 

  13. Botana, F., Valcarce, J.L.: A software tool for the investigation of plane loci. Mathematics and Computers in Simulation 61(2), 141–154 (2003)

    Article  MathSciNet  Google Scholar 

  14. Botana, F., Valcarce, J.L.: Automatic determination of envelopes and other derived curves within a graphic environment. Mathematics and Computers in Simulation 67(1-2), 3–13 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  15. Chou, S.C., Gao, X.S., Zhang, J.Z.: An Introduction to Geometry Expert. In: McRobbie, M.A., Slaney, J.K. (eds.) Automated Deduction - Cade-13. LNCS, vol. 1104, Springer, Heidelberg (1996)

    Google Scholar 

  16. http://www.mmrc.iss.ac.cn/gex/

  17. Chou, S.C., Gao, X.S., Ye, Z.: Java Geometry Expert. In: Proceedings of the 10th Asian Technology Conference in Mathematics, pp. 78–84 (2005)

    Google Scholar 

  18. http://www.cs.wichita.edu/~ye/

  19. Todd, P.: A Constraint Based Interactive Symbolic Geometry System. In: Botana, F., Roanes-Lozano, E. (eds.) ADG 2006. Sixth Intl. Workshop on Automated Deduction in Geometry. Extended Abstracts, Universidad de Vigo, Vigo, Spain, pp. 141–143 (2006)

    Google Scholar 

  20. Roanes-Lozano, E.: Sobre la colaboración de sistemas de geometría dinámica y de álgebra computacional y el nuevo sistema Geometry Expressions. Bol. Soc. Puig Adam 76, 72–90 (2007)

    MathSciNet  Google Scholar 

  21. http://www.geometryexpressions.com/

  22. Roanes-Lozano, E., Roanes-Macías, E.: How Dinamic Geometry could Complement Computer Algebra Systems (Linking Investigations in Geometry to Automated Theorem Proving). In: Procs. of the Fourth Int. DERIVE/TI-89/TI-92 Conference, BK-Teachware, Hagenberg, Austria (2000) (CD-ROM)

    Google Scholar 

  23. Roanes-Lozano, E.: Boosting the Geometrical Possibilities of Dynamic Geometry Systems and Computer Algebra Systems through Cooperation (Plenary Talk). In: Borovcnick, M., Kautschitsch, H. (eds.) Technology in Mathematics Teaching. Procs. of ICTMT-5. Schrifrenreihe Didaktik der Mathematik, öbv&hpt, Wien, Austria, vol. 25, pp. 335–348 (2002)

    Google Scholar 

  24. Roanes-Lozano, E., Roanes-Macías, E., Villar, M.: A Bridge Between Dynamic Geometry and Computer Algebra. Mathematical and Computer Modelling 37(9–10), 1005–1028 (2003)

    Article  MATH  Google Scholar 

  25. Anonymous, The Geometer’s Sketchpad User Guide and Reference Manual, vol. 3. Key Curriculum Press, Berkeley, CA (1995)

    Google Scholar 

  26. Anonymous, The Geometer’s Sketchpad Reference Manual, vol. 4. Key Curriculum Press, Emeryville, CA (2001)

    Google Scholar 

  27. http://www.keypress.com/x5521.xml

  28. Botana, F., Abanades, M.A., Escribano, J.: Computing Locus Equations for Standard Dynamic Geometry Environments. In: Computational Science - ICCS 2007 / CASA 2007 Workshop. LNCS, vol. 4488, pp. 227–234. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  29. http://www.openmath.org

  30. http://www.calques3d.org

  31. Botana, F.: Automatic Determination of Algebraic Surfaces as Loci of Points. In: Sloot, P.M.A., Abramson, D., Bogdanov, A.V., Gorbachev, Y.E., Dongarra, J.J., Zomaya, A.Y. (eds.) ICCS 2003. LNCS, vol. 2657, Springer, Heidelberg (2003)

    Google Scholar 

  32. Roanes-Macías, E., Roanes-Lozano, E.: Automatic determination of geometric loci. 3D-Extension of Simson-Steiner Theorem. In: Campbell, J.A., Roanes-Lozano, E. (eds.) AISC 2000. LNCS (LNAI), vol. 1930, pp. 157–173. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  33. Hestenes, D., Ziegler, R.: Projective Geometry with Clifford Algebra. Acta Applicandae Mathematicae 23, 25–63 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  34. Roanes-Macías, E., Roanes-Lozano, E.: Extensión a IR 3 con seudodivisiones de los teoremas de Simson-Steiner-Guzmán. In: Montes, A. (ed.) Actas del 60 Encuentro de Algebra Computacional y Aplicaciones EACA 2000, Universitat Politecnica de Catalunya, Barcelona, pp. 331–340 (2000)

    Google Scholar 

  35. Roanes-Macías, E., Roanes-Lozano, E.: A Completion of Hypotheses Method for 3D-Geometry. 3D-Extensions of Ceva and Menelaus Theorems. In: Díaz Bánez, J.M., Márquez, A., Portillo, J.R. (eds.) Proceedings of 20th European Workshop on Computational Geometry, Universidad de Sevilla, Seville, pp. 85–88 (2004)

    Google Scholar 

  36. Roanes-Macías, E., Roanes-Lozano, E.: A method for outlining 3D-problems in order to study them mechanically. Application to prove the 3D-version of Desargues Theorem. In: González-Vega, L., Recio, T. (eds.) Proceedings of EACA 2004, Univ. of Cantabria, Santander, Spain, pp. 237–242 (2004)

    Google Scholar 

  37. Buchberger, B.: An Algorithm for Finding a Basis for the Residue Class Ring of a Zero-Dimensional Polynomial Ideal (in German), Ph.D. Thesis. Math. Ins., Univ. of Innsbruck, Innsbruck, Austria (1965)

    Google Scholar 

  38. Buchberger, B.: Applications of Gröbner Bases in non-linear Computational Geometry. In: Rice, J.R. (ed.) Mathematical Aspects of Scientific Software, pp. 59–87. Springer, New York (1988)

    Google Scholar 

  39. Cox, D., Little, J., O’Shea, D.: Ideals, Varieties and Algorithms. Springer, New York (2005)

    Google Scholar 

  40. Wu, W.T.: On the decision problem and the mechanization of theorem-proving in elementary Geometry. A.M.S. Contemporary Mathematics 29, 213–234 (1984)

    Google Scholar 

  41. Wu, W.T.: Some recent advances in Mechanical Theorem-Proving of Geometries. A.M.S. Contemporary Mathematics 29, 235–242 (1984)

    Google Scholar 

  42. Wu, W.T.: Mechanical Theorem Proving in Geometries. In: Text and Monographs in Symbolic Computation, Wien, Springer, Heidelberg (1994)

    Google Scholar 

  43. Chou, S.C.: Mechanical Geometry Theorem Proving. Reidel, Dordrecht (1988)

    MATH  Google Scholar 

  44. Kapur, D., Mundy, J.L.: Wu’s method and its application to perspective viewing. In: Kapur, D., Mundy, J.L. (eds.) Geometric Reasoning, pp. 15–36. MIT Press, Cambridge MA (1989)

    Google Scholar 

  45. Recio, T., Vélez, M.P.: Automatic Discovery of Theorems in Elementary Geometry. Journal of Automated Reasoning 23, 63–82 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  46. Davis, H.: Menelaus and Ceva Theorems and its many applications, http://hamiltonious.virtualave.negt/essays/othe/finalpaper4.htm

  47. de Guzmán, M.: An Extension of the Wallace-Simson Theorem: Projecting in Arbitrary Directions. Mathematical Monthly 106, 574–580 (1999)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universidad Complutense de Madrid, Facultad de Educación, Dept. de Algebra, c/ Rector Royo Villanova s/n, 28040-Madrid, Spain

    Eugenio Roanes-Macías & Eugenio Roanes-Lozano

Authors
  1. Eugenio Roanes-Macías
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Eugenio Roanes-Lozano
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Francisco Botana Tomas Recio

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Roanes-Macías, E., Roanes-Lozano, E. (2007). A Maple Package for Automatic Theorem Proving and Discovery in 3D-Geometry. In: Botana, F., Recio, T. (eds) Automated Deduction in Geometry. ADG 2006. Lecture Notes in Computer Science(), vol 4869. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-77356-6_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-77356-6_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-77355-9

  • Online ISBN: 978-3-540-77356-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation