nach oben

Mathematics in Computer Science

Erschienen in:

25.06.2020

Automated Deduction and Knowledge Management in Geometry

verfasst von: Pedro Quaresma

Erschienen in: Mathematics in Computer Science | Ausgabe 4/2020

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Vorheriger Artikel Foreword to the Special Focus on Automated Deduction in Geometry

Nächster Artikel A Symbolic Dynamic Geometry System Using the Analytical Geometry Method

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

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\)).

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).

JGEX is no longer being developed.

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.

https://www.edukera.com/.

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

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

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

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

https://www.geogebra.org/.

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

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.

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

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

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

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)

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)

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)

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

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)

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)

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)

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)

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

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

13.

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

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)MathSciNetMATH

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)MathSciNetMATH

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)

17.

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

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

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)

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

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)MathSciNetMATH

24.

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

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)

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)

32.

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

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)

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)

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)

38.

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

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)

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

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

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)

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)

48.

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

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

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)MathSciNetMATH

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

54.

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

55.

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

56.

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

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)

61.

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

62.

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

63.

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

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)

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)

66.

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

67.

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

68.

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

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)

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)

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)

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)

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

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)

Titel: Automated Deduction and Knowledge Management in Geometry
verfasst von: Pedro Quaresma
Publikationsdatum: 25.06.2020
Verlag: Springer International Publishing
Erschienen in: Mathematics in Computer Science / Ausgabe 4/2020
Print ISSN: 1661-8270
Elektronische ISSN: 1661-8289
DOI: https://doi.org/10.1007/s11786-020-00489-7

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 4/2020

A Symbolic Dynamic Geometry System Using the Analytical Geometry Method

Automated Detection of Interesting Properties in Regular Polygons

A System for Automated Deduction in Engineering Mechanics

On n-sectors of the Angles of an Arbitrary Triangle

Foreword to the Special Focus on Automated Deduction in Geometry

Premium Partner