Nothing Special   »   [go: up one dir, main page]
Skip to main content
SpringerLink
Log in

Automated Deduction and Knowledge Management in Geometry

  • Published:
Mathematics in Computer Science Aims and scope Submit manuscript

Abstract

Scientific research and education at all levels are concerned primarily with the discovery, verification, communication, and application of scientific knowledge. Learning, reusing, inventing, and archiving are the four essential aspects of knowledge accumulation in mankind’s civilisation process. In this cycle of knowledge accumulation, which has been supported for thousands of years by written books and other physical means, rigorous reasoning has always played an essential role. Nowadays this process is becoming more and more effective due to the availability of new paradigms based on computer applications. Geometric reasoning with such computer applications is one of the most attractive challenges for future accumulation and dissemination of knowledge.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

Notes

  1. The Pythagoras difference is a generalisation of the Pythagoras equality regarding the three sides of a right triangle, to an expression applicable to any triangle (for a triangle ABC with the right angle at B, it holds that \(\mathcal {P}_{ABC}=0\)).

  2. Coherent logic is a fragment of (finitary) first-order logic which allows only the connectives and quantifiers \(\wedge \) (and), \(\vee \) (or), \(\top \) (true), \(\bot \) (false), \(\exists \) (existential quantifier).

  3. JGEX is no longer being developed.

  4. Portfolio problem solving is an approach in which for an individual instance of a specific problem, one particular, hopefully most appropriate, solving technique is automatically selected among several available ones and used. The selection usually employs machine learning methods.

  5. https://www.edukera.com/.

  6. The OpenGeometryProver github project: https://github.com/opengeometryprover/.

  7. http://hilbert.mat.uc.pt/TGTP/.

  8. https://prover-test.geogebra.org/job/GeoGebra-provertest/ws/test/scripts/benchmark/prover/html/all.html.

  9. http://hilbert.mat.uc.pt/GeoThms/.

  10. https://www.geogebra.org/.

  11. https://www.geogebra.org/materials.

  12. We consider that every concept of the graph represents a distinct geometric object. Whenever inference reveals that two concepts represent the same object, they are merged.

  13. Pedro Quaresma and Pierluigi Graziani, Measuring the Readability of a Proof, in preparation.

  14. AIED2019, Workshop on Intelligent Textbooks, http://ml4ed.cc/2019-AIED-workshop/.

References

  1. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development (Coq’Art: The Calculus of Inductive Constructions). Springer, EATCS (2004)

  2. Botana, F., Hohenwarter, M., Janičić, P., Kovács, Z., Petrović, Ivan, R., Tomás, W.S.: Automated theorem proving in GeoGebra: current achievements. J. Autom. Reason. 55(1), 39–59 (2015)

  3. Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems: 25 Years of TACAS: TOOLympics, Volume 11429 of LNCS. Springer, 2019. Held as Part of ETAPS 2019, Prague, Czech Republic, April 6–11 (2019)

  4. Botana, F., Kovács, Z., Recio, T.: Towards an automated geometer. In: Fleuriot, J., Wang, D., Calmet, J. (eds.) Artificial Intelligence and Symbolic Computation, pp. 215–220. Springer, Cham (2018)

    Google Scholar 

  5. Botana, F., Valcarce, J.L.: A dynamic-symbolic interface for geometric theorem discovery. Comput. Educ. 38, 21–35 (2002)

    Google Scholar 

  6. Baeta, N., Quaresma, P.: The full angle method on the OpenGeoProver. In: Lange, C., Aspinall, D., Carette, J., Davenport, J., Kohlhase, A., Kohlhase, M., Libbrecht, P., Quaresma, P., Rabe, F., Sojka, P., Whiteside, I., Windsteiger, W. (eds.) MathUI, OpenMath, PLMMS and ThEdu Workshops and Work in Progress at the Conference on Intelligent Computer Mathematics, number 1010 in CEUR Workshop Proceedings, Aachen (2013)

  7. Baeta, N., Quaresma, P.: Towards ranking geometric automated theorem provers. In: Quaresma, P., Neuper, W. (eds.) Proceedings 7th International Workshop on Theorem proving components for Educational software, Oxford, United Kingdom, 18 July 2018, volume 290 of Electronic Proceedings in Theoretical Computer Science, pp. 30–37. Open Publishing Association (2019)

  8. Baeta, N., Quaresma, P., Kovács, Z.: Towards a geometry automated provers competition. In: Proceedings 8th International Workshop on Theorem proving Components for Educational Software, Volume 313 of Electronic Proceedings in Theoretical Computer Science, pp. 93–100, February 2020. (ThEdu’19), Natal, Brazil, 25th August (2019)

  9. Budd Rowe, M.: Wait-time and rewards as instructional variables: Their influence on language, logic, and fate control. Technical report, National Association for Research in Science Teaching (1972)

  10. Budd Rowe, M.: Wait time: slowing down may be a way of speeding up!. J. Teach. Educ. 37(1), 43–50 (1986)

    Google Scholar 

  11. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude—A High-Performance Logical Framework (Pb). Lecture Notes in Computer Science, vol. 4350. Springer, New York (2007)

    MATH  Google Scholar 

  12. Chou, S.-C., Gao, X.-S.: Automated reasoning in geometry. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 707–749. Elsevier, Amsterdam (2001)

    MATH  Google Scholar 

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

    MATH  Google Scholar 

  14. Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Automated generation of readable proofs with geometric invariants, I. Multiple and shortest proof generation. J. Autom. Reason. 17(13), 325–347 (1996)

    MathSciNet  MATH  Google Scholar 

  15. Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Automated generation of readable proofs with geometric invariants, II. Theorem proving with full-angles. J. Autom. Reason. 17(13), 349–370 (1996)

    MathSciNet  MATH  Google Scholar 

  16. Chen, X.: Electronic geometry textbook: a geometric textbook knowledge management system. Intelligent Computer Mathematics. Number 6167 in LNCS, pp. 278–292. Springer, Berlin (2010)

    Google Scholar 

  17. Chen, X.: Representation and automated transformation of geometric statements. J. Syst. Sci. Complex. 27(2), 382–412 (2014)

    MathSciNet  MATH  Google Scholar 

  18. Chou, S.C.: Proving and discovering geometry theorems using Wu’s method. Ph.D. thesis, The University of Texas, Austin (1985)

  19. Chou, S.-C.: Mechanical Geometry Theorem Proving. D. Reidel Publishing Company, Dordrecht (1987)

    MATH  Google Scholar 

  20. Chen, X., Li, W., Luo, J., Wang, D.: Open geometry textbook: a case study of knowledge acquisition via collective intelligence. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) Intelligent Computer Mathematics, pp. 432–437. Springer, Berlin (2012)

    Google Scholar 

  21. Chein, M., Mugnier, M.-L.: Graph-Based Knowledge Representation: Computational Foundations of Conceptual Graphs. Advanced Information and Knowledge Processing Series. Springer, New York (2009)

    MATH  Google Scholar 

  22. Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) Automata Theory and Formal Languages 2nd GI Conference Kaiserslautern, May 20–23, 1975. Lecture Notes in Computer Science, vol. 33. Springer, Berlin (1975)

  23. Coelho, H., Pereira, L.M.: Automated reasoning in geometry theorem proving with Prolog. J. Autom. Reason. 2(4), 329–390 (1986)

    MathSciNet  MATH  Google Scholar 

  24. Chen, X., Wang, D.: Management of geometric knowledge in textbooks. Data Knowl. Eng. 73, 43–57 (2012)

    Google Scholar 

  25. de Bruijn, N.G.: A survey of the project Automath. Selected Papers on Automath. Volume 133 of Studies in Logic and the Foundations of Mathematics, pp. 41–161. North-Holland, Amsterdam (1994)

    Google Scholar 

  26. Dhar, S., Roy, S., Das, S.: A Critical Survey of Mathematical Search Engines. In: Computational Intelligence, Communications, and Business Analytics, pp. 193–207. Springer, New York (2019)

  27. Font, L., Richard, P.R., Gagnon, M.: Improving qed-tutrix by automating the generation of proofs. In: Quaresma, P., Neuper, W. (eds.) Proceedings 6th International Workshop on Theorem Proving Components for Educational Software, Gothenburg, Sweden, 6 Aug 2017, volume 267 of Electronic Proceedings in Theoretical Computer Science, pp. 38–58. Open Publishing Association (2018)

  28. Gelernter, H.: Realization of a geometry-theorem proving machine. In: Computers & Thought, 2nd edn., pp. 134–152. MIT Press, Cambridge (1995)

  29. Gelernter, H., Hansen, J.R., Loveland, D.W.: Empirical explorations of the geometry theorem machine. In: Papers Presented at the May 3–5, 1960, Western Joint IRE-AIEE-ACM Computer Conference, IRE-AIEE-ACM ’60 (Western), pp. 143–149. ACM, New York (1960)

  30. Gagnon, M., Leduc, N., Richard, P.R., Tessier-Baillargeon, M.: Qed-tutrix: creating and expanding a problem database towards personalized problem itineraries for proof learning in geometry. In: Proceedings of the Tenth Congress of the European Society for Research in Mathematics Education (CERME10) (2017)

  31. Hanna, G.: Proof, explanation and exploration: an overview. Educ. Stud. Math. 44(1–2), 5–23 (2000)

    Google Scholar 

  32. Hearst, M.A.: Search User Interfaces. Cambridge University Press, Cambridge (2009)

    Google Scholar 

  33. Han, T.A., Pereira, L.M., Lenaerts, T.: Modelling and influencing the AI bidding war: a research agenda. In: AAAI/ACM Conference on AI, Ethics and Society 2019, vol. 1 (2019)

  34. Haralambous, Y., Quaresma, P.: Querying geometric figures using a controlled language, ontological graphs and dependency lattices. In: Watt, S., et al. (eds.) CICM 2014, Volume 8543 of LNAI, pp. 298–311. Springer, New York (2014)

    Google Scholar 

  35. Haralambous, Y., Quaresma, P.: Geometric search in TGTP. In: Li, H. (ed.) Proceedings of the 12th International Conference on Automated Deduction in Geometry. SMS International (2018)

  36. Hanna, G., Reid, D., de Villiers, M. (eds.): Proof Technology in Mathematics Research and Teaching. Springer, New York (2019)

    Google Scholar 

  37. Janičić, P.: GCLC—a tool for constructive euclidean geometry and more than that. In: Iglesias, A., Takayama, N. (eds.) Mathematical Software—ICMS 2006, Volume 4151 of Lecture Notes in Computer Science, pp. 58–73. Springer, New York (2006)

    Google Scholar 

  38. Janičić, P., Narboux, J., Quaresma, P.: The Area method: a recapitulation. J. Autom. Reason. 48(4), 489–532 (2012)

    MathSciNet  MATH  Google Scholar 

  39. Janičić, P., Quaresma, P.: System description: GCLCprover + GeoThms. In: Furbach, U., Shankar, N. (eds.) Automated Reasoning, Volume 4130 of Lecture Notes in Computer Science, pp. 145–150. Springer, New York (2006)

    Google Scholar 

  40. Janičić, P., Quaresma, P.: Automatic verification of regular constructions in dynamic geometry systems. In: Botana, F., Recio, T. (eds.) Automated Deduction in Geometry, Volume 4869 of Lecture Notes in Computer Science, pp. 39–51. Springer, New York (2007)

    MATH  Google Scholar 

  41. Kapur, D.: Geometry theorem proving using Hilbert’s nullstellensatz. In: SYMSAC ’86: Proceedings of the fifth ACM symposium on Symbolic and algebraic computation, pp. 202–208. ACM Press, New York (1986)

  42. Kapur, D.: Using Gröbner bases to reason about geometry problems. J. Symb. Comput. 2(4), 399–408 (1986)

    MATH  Google Scholar 

  43. Kortenkamp, U., Dohrmann, C., Kreis, Y., Dording, C., Libbrecht, P., Mercat, C.: Using the Intergeo platform for teaching and research. In: Proceedings of the 9th International Conference on Technology in Mathematics Teaching (ICTMT-9) (2009)

  44. Kovács, Z.: The relation tool in geogebra 5. In: Botana, F., Quaresma, P. (eds.) Automated Deduction in Geometry, pp. 53–71. Springer, New York (2015)

    Google Scholar 

  45. Leduc, N.: QED-Tutrix : système tutoriel intelligent pour l’accompagnement d’élèves en situation de résolution de problèmes de démonstration en géométrie plane. Ph.D. thesis, École polytechnique de Montréal (2016)

  46. Lemoine, É.: Géométrographie ou Art des constructions géométriques, volume 18 of Phys-Mathématique. Scentia, Sydney (1902)

  47. Li, H.: Clifford algebra approaches to mechanical geometry theorem proving. In: Gao, X.-S., Wang, D. (eds.) Mathematics Mechanization and Applications, pp. 205–299. Academic Press, San Diego (2000)

    Google Scholar 

  48. Mackay, J.S.: The geometrography of euclid’s problems. Proc. Edinb. Math. Soc. 12, 2–16 (1893)

    MATH  Google Scholar 

  49. Meseguer, J.: Twenty years of rewriting logic. In: Ölveczky, P.C. (ed.) Rewriting Logic and Its Applications, pp. 15–17. Springer, Berlin (2010)

    MATH  Google Scholar 

  50. Kovács, Z., Nikolić, P., Mladen, J., Marinković, V.: Portfolio theorem proving and prover runtime prediction for geometry. Ann. Math. Artif. Intell. 85, 119–146 (2019)

    MathSciNet  MATH  Google Scholar 

  51. Moraes, T.G., Santoro, F.M., Borges, M.R.S.: Tabulæ: educational groupware for learning geometry. In: Fifth IEEE International Conference on Advanced Learning Technologies, 2005. ICALT 2005, pp. 750–754 (2005)

  52. Moriyón, R., Saiz, F., Mora, M.: GeoThink: An Environment for Guided Collaborative Learning of Geometry, volume 4 of Nuevas Ideas en Informática Educativa, pp. 200–2008. J. Sánchez (ed.), Santiago de Chile (2008)

  53. Mathis, P., Thierry, S.E.B.: A formalization of geometric constraint systems and their decomposition. Formal Asp. Comput. 22(2), 129–151 (2010)

    MATH  Google Scholar 

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

    MATH  Google Scholar 

  55. Pambuccian, V.: The simplest axiom system for plane hyperbolic geometry. Stud. Log. 77(3), 385–411 (2004)

    MathSciNet  MATH  Google Scholar 

  56. Pinheiro, V.A.: Geometrografia 1. Bahiense, Rio de Janeiro (1974)

    Google Scholar 

  57. Petrović, I., Kovács, Z., Weitzhofer, S., Hohenwarter, M., Janičić, P.: Extending GeoGebra with automated theorem proving by using OpenGeoProver. In: Proceedings CADGME 2012, Novi Sad, Serbia (2012)

  58. Quaresma, P., Baeta, N.: Geometry automated theorem provers systems competition 0.2 report. Techreport 1, CISUC (2019)

  59. Quaresma, P., Nuno, B.: Current status of the I2GATP common format. In: Botana, F., Quaresma, P. (eds.) Proceedings ADG 2014, Volume 2014 of CISUC Technical Report, pp. 67–74. CISUC (2014)

  60. Quaresma, P., Santos, V.: Computer-generated geometry proofs in a learning context. In: Hanna, G., Reid, D.A., de Villiers, M. (eds.) Proof Technology in Mathematics Research and Teaching. Springer, New York (2019)

    Google Scholar 

  61. Quaresma, P., Santos, V., Graziani, P., Baeta, N.: Taxonomy of geometric problems. J. Symb. Comput. 97, 31–55 (2020)

    MATH  Google Scholar 

  62. Quaresma, P., Santos, V., Marić, M.: WGL, a web laboratory for geometry. Educ. Inf. Technol. 23(1), 237–252 (2018)

    Google Scholar 

  63. Quaife, A.: Automated development of Tarski’s geometry. J. Autom. Reason. 5, 97–118 (1989). https://doi.org/10.1007/BF00245024

    Article  MathSciNet  MATH  Google Scholar 

  64. Quaresma, P.: Thousands of geometric problems for geometric Theorem Provers (TGTP). In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) Automated Deduction in Geometry, volume 6877 of Lecture Notes in Computer Science, pp. 169–181. Springer, New York (2011)

    Google Scholar 

  65. Quaresma, P.: Automatic deduction in an AI geometry book. In: Fleuriot, J., Wang, D., Calmet, J. (eds.) Artificial Intelligence and Symbolic Computation, volume 11110 of Lecture Notes in Computer Science, pp. 221–226. Springer, New York (2018)

    Google Scholar 

  66. Richter-Gebert, J., Kortenkamp, U.: The Interactive Geometry Software Cinderella. Springer, New York (1999)

    MATH  Google Scholar 

  67. Recio, T., Vélez, M.P.: Automatic discovery of theorems in elementary geometry. J. Autom. Reason. 23, 63–82 (1999)

    MathSciNet  MATH  Google Scholar 

  68. Santos, V., Baeta, N., Quaresma, P.: Geometrography in dynamic geometry. Int. J. Technol. Math. Educ. 26(2), 89–96 (2019)

    Google Scholar 

  69. Santiago, E., Hendriks, M., Kreis, Y., Kortenkamp, U., Marquès, D.: i2g Common File Format Final Version. Technical report D3.10, The Intergeo Consortium (2010)

  70. Stojanović, S., Pavlović, V., Janičić, P.: A coherent logic based geometry theorem prover capable of producing formal and readable proofs. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) Automated Deduction in Geometry, Volume 6877 of Lecture Notes in Computer Science, vol. 6877, pp. 201–220. Springer, Berlin (2011)

    Google Scholar 

  71. Stahl, R.J.: Using “think-time” and “wait-time” skillfully in the classroom. Technical report, ERIC Digest (1994)

  72. Sutcliffe, G.: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483–502 (2017)

  73. Tarski, A.: A decision method for elementary algebra and geometry. Technical report, RAND Corporation (1951)

  74. van Dalen, D.: Logic and Structure. Universitext, Springer (1980)

  75. Wang, D.: Reasoning about geometric problems using an elimination method. In: Pfalzgraf, J., Wang, D. (eds.) Automated Pratical Reasoning, pp. 147–185. Springer, New York (1995)

    Google Scholar 

  76. Wang, D., Chen, X., An, W., Jiang, L., Song, D.: Opengeo: an open geometric knowledge base. In: Hong, H., Yap, C. (eds.) Mathematical Software—ICMS 2014, volume 8592 of Lecture Notes in Computer Science, pp. 240–245. Springer, Berlin (2014)

    Google Scholar 

  77. Wiedijk, F.: The de Bruijn factor. Poster at International Conference on Theorem Proving in Higher Order Logics (TPHOL2000), 2000. Portland, Oregon, USA, 14–18 August (2000)

  78. Wu, W.-T.: On the decision problem and the mechanization of theorem proving in elementary geometry. In: Automated Theorem Proving: After 25 Years, Volume 29 of Contemporary Mathematics, pp. 213–234. American Mathematical Society (1984)

  79. Wong, W.-K., Yin, S.-K., Yang, H.-H., Cheng, Y.-H.: Using computer-assisted multiple representations in learning geometry proofs. Educ. Technol. Soc. 14(3), 43–54 (2011)

    Google Scholar 

  80. Ye, Z., Chou, S.-C., Gao, X.-S.: Visually dynamic presentation of proofs in plane geometry, part 1. J. Autom. Reason. 45, 213–241 (2010)

    MATH  Google Scholar 

  81. Ye, Z., Chou, S.-C., Gao, X.-S.: An introduction to Java geometry expert. In: Sturm, T., Zengler, C. (eds.) Automated Deduction in Geometry, Volume 6301 of Lecture Notes in Computer Science, pp. 189–195. Springer, Berlin (2011)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CISUC, Department of Mathematics, University of Coimbra, Coimbra, Portugal

    Pedro Quaresma

Authors
  1. Pedro Quaresma
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Pedro Quaresma.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

This work is funded by national funds through the FCT-Foundation for Science and Technology, I.P., within the scope of the project CISUC-UID/CEC/00326/2020 and by European Social Fund, through the Regional Operational Program Centro 2020.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Quaresma, P. Automated Deduction and Knowledge Management in Geometry. Math.Comput.Sci. 14, 673–692 (2020). https://doi.org/10.1007/s11786-020-00489-7

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11786-020-00489-7

Keywords

Mathematics Subject Classification

Search

Navigation