nach oben

Mathematics in Computer Science

Erschienen in:

01.12.2022

Is Computer Algebra Ready for Conjecturing and Proving Geometric Inequalities in the Classroom?

verfasst von: Christopher W. Brown, Zoltán Kovács, Tomás Recio, Róbert Vajda, M. Pilar Vélez

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

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

We introduce an experimental version of GeoGebra that successfully conjectures and proves a large scale of geometric inequalities by providing an easy-to-use graphical interface. GeoGebra Discovery includes an embedded version of the Tarski/QEPCAD B system which can solve a real quantifier elimination problem, so the input geometric construction can be translated into a semi-algebraic system, and after some algebraic manipulations, the obtained formula can be translated back to a precisely stated geometric inequality. We provide some non-trivial examples to illustrate the performance of GeoGebra Discovery when dealing with inequalities, as well as some technical difficulties.

Vorheriger Artikel How Many Structure Constants do Exist in Riemannian Geometry?

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

See [2]. It is inequality 4.2. on page 31. We have followed the precise formulation of this author, a well known authority in the field of triangle inequalities.

Available for download at https://www.cypress.io/.

See https://matek.hu/zoltan/compare-20211228/all.html for the detailed results.

See https://matek.hu/zoltan/proverrg-20211228/all.html.

Abar, C. A. A. P., Kovács, Z., Recio, T., Vajda, R.: Conectando Mathematica e GeoGebra para explorar construções geométricas planas. Presentation at Wolfram Technology Conference, Saõ Paulo, Brazil, November (2019)

Bottema, O.: Inequalities for \(R\), \(r\) and \(s\). Publikacije Elektrotehničkog Fakulteta. Serija Matematika i Fizika, 338/352:27–36, (1971)

Bottema, O., Djordjevic, R., Janic, R., Mitrinovic, D., Vasic, P.: Geometric Inequalities. Wolters-Noordhoff Publishing, Groningen (1969)MATH

Bright, P.: The Web is getting its bytecode: WebAssembly. Condé Nast (2015)

Brown, C., Davenport, J.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In Proceedings of ISSAC ’07, 54–60. ACM, (2007)

Brown, C.W.: An overview of QEPCAD B: a tool for real quantifier elimination and formula simplification. J. Jpn. Soc. Symb. Algebr. Comput. 10(1), 13–22 (2003)

Bulmer, M., Fearnley-Sander, D., Stokes, T.: The kinds of truth of geometry theorems. In: Richter-Gebert, J., Wang, D. (eds.) Automated Deduction in Geometry. Lecture Notes in Computer Science 2061, pp. 129–143. Springer, Berlin (2001)MATH

Chen, C., Maza, M.M.: Quantifier elimination by cylindrical algebraic decomposition based on regular chains. J. Symb. Comput. 75, 74–93 (2016)MathSciNetCrossRefMATH

Chou, S.C.: Mechanical Geometry Theorem Proving. D. Reidel Publishing Company, Dordrecht, Netherlands (1988)MATH

10.

Collins, G.: Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. Lect. Notes Comput. Sci. 33, 134–183 (1975)CrossRef

11.

Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 12, 299–328 (1991)MathSciNetCrossRefMATH

12.

Conti, P., Traverso, C.: A case of automatic theorem proving in Euclidean geometry: the Maclane 83 theorem. In: Cohen, G., Giusti, M., Mora, T. (eds.) Applied Algebra. Algebraic Algorithms and Error-Correcting Codes. Lecture Notes in Computer Science, Springer, Berlin (1995)

13.

Conti, P., Traverso, C.: Algebraic and semialgebraic proofs: methods and paradoxes. In: Richter-Gebert, J., Wang, D. (eds.) Automated Deduction in Geometry. Lecture Notes in Computer Science, pp. 83–103. Springer, Berlin (2001)CrossRef

14.

Davenport, J., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput., 5(1)

15.

Dolzmann, A., Sturm, T.: Redlog: computer algebra meets computer logic. ACM SIGSAM Bull. 31(2), 2–9 (1997)CrossRef

16.

Dolzmann, A., Sturm, T., Weispfenning, V.: A new approach for automatic theorem proving in real geometry. J. Autom. Reason. 21(3), 357–380 (1998)MathSciNetCrossRefMATH

17.

Erdős, P.: Problem 3740. Amer. Math. Mon. 42, 396 (1935)

18.

Guergueb, A., Mainguené, J., Roy, M.F.: Examples of automatic theorem proving in real geometry. In: ISSAC-94, 20–23, ACM press, (1994)

19.

Hanna, G., Yan, X.: Opening a discussion on teaching proof with automated theorem provers. Learn. Math. 41(3), 42–46 (2021)

20.

Hohenwarter, M., Kovács, Z., Recio, T.: Using Automated Reasoning Tools to Explore Geometric Statements and Conjectures, 215–236. Springer International Publishing, Cham (2019)

21.

Iwane, H., Yanami, H., Anai, H.: SyNRAC: a toolbox for solving real algebraic constraints. In Proceedings of ICMS-2014. LNCS, vol. 8592

22.

Kovács, Z.: GeoGebra Discovery. A GitHub project, 07 2020. https://github.com/kovzol/geogebra-discovery

23.

Kovács, Z., Recio, T., Richard, P. R., Vaerenbergh, S. V., Vélez, M. P.: Towards an ecosystem for computer-supported geometric reasoning. Int. J. Math. Edu. Sci. Technol. (2020)

24.

Kovács, Z., Recio, T., Tabera, L.F., Vélez, M.P.: Dealing with degeneracies in automated theorem proving in geometry. Mathematics 9(16), 1964 (2021)CrossRef

25.

Kovács, Z., Recio, T., Vélez, M.P.: Using automated reasoning tools in GeoGebra in the teaching and learning of proving in geometry. Int. J. Technol. Math. Edu. 25(2), 33–50 (2018)

26.

Kovács, Z., Recio, T., Vélez, M.P.: Detecting truth, just on parts. Revista Matemática Complutense 32(2), 451–474 (2019)MathSciNetCrossRefMATH

27.

Kovács, Z., Recio, T., Vélez, M. P.: Approaching Cesáro’s inequality through GeoGebra Discovery”. In: Proceedings of the 26th Asian Technology Conference in Mathematics, W. C. Yang, D. B. Meade, M. Majewski (eds), 160–174. Mathematics and Technology, LL, Dec. 13–15, 2021

28.

M. Ladra, P. Páez-Guillán, T. Recio. Dealing with negative conditions in automated proving: tools and challenges. The unexpected consequences of Rabinowitsch’s trick. Revista de la Real Academia de Ciencias Exactas, Físicas y Naturales (RACSAM), 114(4), 2020

29.

Mordell, L.J., Barrow, D.F.: Solution to 3740. Amer. Math. Mon. 44, 252–254 (1937)

30.

T. Recio, F. Botana. Where the truth lies (in Automatic Theorem Proving in Elementary Geometry). In: Proceedings of international conference on computational science and its applications 2004, Lecture Notes in Computer Science 3044:761–771, Springer, 2004

31.

Recio, T., Losada, R., Kovács, Z., Ueno, C.: Discovering geometric inequalities: the concourse of geoGebra discovery, dynamic coloring and maple tools. Mathematics 9(20), 2548 (2021)CrossRef

32.

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

33.

Reiman, I.: Fejezetek az elemi geometriából. Typotex, Budapest (2002)

34.

Sturm, T.: A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications. Math. Comput. Sci. 11, 483–502 (2017)MathSciNetCrossRefMATH

35.

Tarski, A.A., Decision Method, A., for Elementary Algebra and Geometry. Manuscript. Santa Monica, CA: RAND Corp.,: Republished as A Decision Method for Elementary Algebra and Geometry, 2nd edn., p. 1951. University of California Press, Berkeley, CA (1948)

36.

Vajda, R., Kovács, Z.: GeoGebra and the realgeom reasoning tool. CEUR Workshop Proceedings 2752, 204–219 (2020)

37.

Vale-Enriquez, F., Brown, C.: Polynomial constraints and unsat cores in Tarski. In: Mathematical Software - ICMS 2018. LNCS, vol. 10931, pp. 466–474. Springer, Cham (2018)

38.

Wolfram Research, Inc. Mathematica, version 12.1, 2020. Champaign, IL

39.

Wu, W.T.: On the decision problem and the mechanization of theorem proving in elementary geometry. Sci. Sinica 21, 157–179 (1978)MathSciNet

40.

Xia, B., Yang, L.: Automated Inequality Proving And Discovering. World Scientific, Singapore (2017)MATH

41.

Yang, L., Xia, B.: Automated deduction in real geometry. In: Chen, F., Wang, D. (eds.) Lecture Notes Series on Computing Volume 11: Geometric Computation, pp. 248–298. World Scientific, Singapore (2004)

Titel: Is Computer Algebra Ready for Conjecturing and Proving Geometric Inequalities in the Classroom?
verfasst von: Christopher W. Brown
Zoltán Kovács
Tomás Recio
Róbert Vajda
M. Pilar Vélez
Publikationsdatum: 01.12.2022
Verlag: Springer International Publishing
Erschienen in: Mathematics in Computer Science / Ausgabe 4/2022
Print ISSN: 1661-8270
Elektronische ISSN: 1661-8289
DOI: https://doi.org/10.1007/s11786-022-00532-9

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/2022

Memories of Vladimir Gerdt

Vladimir Gerdt: A Computer Algebra Enthusiast

30 Years with Vladimir Gerdt

How Many Structure Constants do Exist in Riemannian Geometry?

SMS Nanning and RWTH Aachen: In Memory of Vladimir Gerdt

A New Type of Difference Dimension Polynomials

Premium Partner