Skip to main content
SpringerLink
Log in

Geometry Constructions Language

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

Abstract

Geometry Constructions Language (gcl) is a language for explicit descriptions of constructions in Euclidean plane and of their properties. Other mathematical objects can also be described in the language. The language gcl is intuitive and simple, yet it supports arrays, flow control structures, user-defined procedures, etc. The processors for the gcl language—applications gclc and Wingclc—enable visualization of described objects and producing of mathematical illustrations, provide different semantical information and support for automated proving of properties of the constructed objects. These features make the tools gclc and Wingclc powerful mechanized geometry systems and they have thousands of users worldwide.

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

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Bertot, Y., Guilhot, F., Pottier, L.: Visualizing geometrical statements with geoview. Electron. Notes Theor. Comput. Sci. 103, 49–65 (2004)

    Article  Google Scholar 

  2. Bezem, M., Coquand, T.: Automating coherent logic. In: Sutcliffe, G., Voronkov, A. (eds.) 12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning—LPAR 2005. Lecture Notes in Computer Science, vol. 3835. Springer, Berlin (2005)

    Chapter  Google Scholar 

  3. Botana, F.: A web-based intelligent system for geometric discovery. In: International Conference on Computational Science. Lecture Notes in Computer Science, vol. 2657, pp. 801–810. Springer, Berlin (2003)

    Google Scholar 

  4. Botana, F.: Format exchange in dynamic geometry. In: Workshop Intergeo-España (2007)

  5. Botana, F., Recio, T.: Towards solving the dynamic geometry bottleneck via a symbolic approach. In: Automated Deduction in Geometry. Lecture Notes in Computer Science, vol. 3763, pp. 92–110. Springer, Berlin (2006)

    Chapter  Google Scholar 

  6. Botana, F., Valcarce, J.: A dynamicsymbolic interface for geometric theorem discovery. Comput. Educ. 38, 21–35 (2002)

    Article  Google Scholar 

  7. Chou, C.C., Gao, X.S., Zhang, J.Z.: Automated production of traditional proofs for constructive geometry theorems. In: Eighth Annual IEEE Symposium on Logic in Computer Science (1993)

  8. Chou, S.C., Gao, X.S., Zhang, J.Z.: Machine Proofs in Geometry. World Scientific, Singapore (1994)

    MATH  Google Scholar 

  9. Chou, S.C., Gao, X.S., Zhang, J.Z.: An introduction to geometry expert. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 13. Lecture Notes in Artificial Intelligence, vol. 1104. Springer, Berlin (1996)

    Google Scholar 

  10. Djorić, M., Janičić, P.: Constructions, instructions, interactions. Teach. Math. Appl. 23(2), 69–88 (2004)

    Article  Google Scholar 

  11. Lučić, Z., et. al.: Euclid’s Elements. Online at http://www.matf.bg.ac.rs/~zlucic/ (2009)

  12. Buchberger, B., et al.: Theorema: towards computer-aided mathematical theory exploration. J. Appl. Logic 4, 359–652 (2006)

    Article  MathSciNet  Google Scholar 

  13. Fisher, J., Bezem, M.: Skolem machines and geometric logic. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) 4th International Colloquium on Theoretical Aspects of Computing—ICTAC 2007. Lecture Notes in Computer Science, vol. 4711. Springer, Berlin (2007)

    Chapter  Google Scholar 

  14. Gao, X.-S., Lin, Q.: Mmp/geometer a software package for automated geometric reasoning. In: Winkler, F. (ed.) Automated Deduction in Geometry: 4th International Workshop, (ADG 2002). Lecture Notes in Computer Science, vol. 2930, pp. 44–66. Springer, Berlin (2004)

    Google Scholar 

  15. Hohenwarter, M., Fuchs, K.: Combination of dynamic geometry, algebra and calculus in the software system GeoGebra. In: Proceedings of Computer Algebra Systems and Dynamic Geometry Systems in Mathematics Teaching Conference (2004)

  16. Janičić, P.: GCLC – a tool for constructive Euclidean geometry and more than that. In: Takayama, N., Iglesias, A., Gutierrez, J. (eds.) Proceedings of International Congress of Mathematical Software (ICMS 2006). Lecture Notes in Computer Science, vol. 4151, pp. 58–73. Springer, Berlin (2006)

    Google Scholar 

  17. Janičić, P., Quaresma, P.: System description: Gclcprover + GeoThms. In: Furbach, U., Shankar, N. (eds) International Joint Conference on Automated Reasoning (IJCAR-2006). Lecture Notes in Artificial Intelligence, vol. 4130, pp. 145–150. Springer, Berlin (2006)

    Google Scholar 

  18. Janičić, P.: Zbirka zadataka iz geometrije. Skripta Internacional, Beograd, 1st edition 1997, 6th edition 2005. Collection of problems in geometry (in Serbian)

  19. Janičić, P., Quaresma, P.: Automatic verification of regular constructions in dynamic geometry systems. In: Botana, F., Recio, T. (eds.) Automated Deduction in Geometry. Lecture Notes in Artificial Intelligence, vol. 4869, pp. 39–51. Springer, Berlin (2007)

    Google Scholar 

  20. Janičić, P., Trajković, I.: WinGCLC—a workbench for formally describing figures. In: Proceedings of the 18th Spring Conference on Computer Graphics (SCCG 2003), pp. 251–256. Budmerice, Slovakia, ACM, New York (2003)

  21. Knuth, D.: TeXBook. Addison Wesley Professional, Reading (1986)

    Google Scholar 

  22. Kortenkamp, U., Richter-Gebert, J.: Using automatic theorem proving to improve the usability of geometry software. In: Workshop on Mathematical User Interfaces (2004)

  23. Lamport, L.: LaTeX: a Document Preparation System. Addison Wesley Professional, Reading (1994)

    Google Scholar 

  24. Liang, T., Wang, D.: Towards a geometric-object-oriented language. In: Hong, H., Wang, D. (eds.) Automated Deduction in Geometry. Lecture Notes in Computer Science, vol. 3763, pp. 130–155. Springer, Berlin (2006)

    Chapter  Google Scholar 

  25. Liang, T., Wang, D.: On the design and implementation of a geometric-object-oriented language. Front. Comput. Sci. China 1(2), 180–190 (2007)

    Article  Google Scholar 

  26. Matsuda, N., Vanlehn, K.: Gramy: a geometry theorem prover capable of construction. J. Autom. Reason. 32, 3–33 (2004)

    Article  MathSciNet  Google Scholar 

  27. Narboux, J.: A graphical user interface for formal proofs in geometry. J. Autom. Reason. 39(2), 161–180 (2007)

    Article  MATH  Google Scholar 

  28. Narboux, J.: Geoproof, a user interface for formal proofs in geometry. In: Mathematical User-Interfaces Workshop (2007)

  29. Predović, G.: Automated geometry theorem proving based on Wu’s and Buchberger’s methods. Master’s thesis, Faculty of Mathematics, University of Belgrade, supervisor: Predrag Janičić (2008)

  30. Quaresma, P., Janičić, P.: Integrating dynamic geometry software, deduction systems, and theorem repositories. In: Borwein, J.M., Farmer, W.M. (eds.) Mathematical Knowledge Management (MKM-2006). Lecture Notes in Artificial Intelligence, vol. 4108, pp. 280–294. Springer, Berlin (2006)

    Chapter  Google Scholar 

  31. Quaresma, P., Janičić, P.: Geothms—a web system for Euclidean constructive geometry. Electron. Notes Theor. Comput. Sci. 174(2), 35–48 (2007)

    Article  Google Scholar 

  32. Quaresma, P., Janičić, P.: Framework for the constructive geometry. Technical Report TR2006/001, Center for Informatics and Systems of the University of Coimbra (2006)

  33. Quaresma, P., Janičić, P., Tomašević, J., Vujošević-Janičić, M., Tošić, D.: XML-based format for geometry—XML-based format for descriptions of geometrical constructions and geometrical proofs. In: Borwein, J.M., Rocha, E.M., Rodrigues, J.F. (eds.) Communicating Mathematics in Digital Era, pp. 183–197. A K Peters, Wellesley (2008)

    Google Scholar 

  34. Wang, D.: Geother 1.1: handling and proving geometric theorems automatically. In: Automated Deduction in Geometry. Lecture Notes in Artificial Intelligence, vol. 2930, pp. 194–215. Springer, Berlin (2004)

    Google Scholar 

  35. Wilson, S., Fleuriot, J.: Combining dynamic geometry, automated geometry theorem proving and diagrammatic proofs. In: Workshop on User Interfaces for Theorem Provers (UITP) (2005)

  36. Ye, Z., Chou, S.-C., Gao, X.-S.: An introduction to java geometry expert. In: Automated Deduction in Geometry (2008)

Download references

Author information

Authors and Affiliations

  1. Faculty of Mathematics, University of Belgrade, Studentski trg 16, 11 000, Belgrade, Serbia

    Predrag Janičić

Authors
  1. Predrag Janičić
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Predrag Janičić.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Janičić, P. Geometry Constructions Language. J Autom Reasoning 44, 3 (2010). https://doi.org/10.1007/s10817-009-9135-8

Download citation

  • Received:

  • Accepted:

  • Published:

  • DOI: https://doi.org/10.1007/s10817-009-9135-8

Keywords

Search

Navigation