30 July 2024
Automated measuring the difficulty of geometric theorems
This entry summarizes some achieved results and the planned future work on
automated measuring the difficulty of geometric theorems.
Some references for the newcomers:
- Z. K., Tomás Recio, M. Pilar Vélez:
Showing Proofs, Assessing Difficulty with GeoGebra Discovery.
In Pedro Quaresma and Zoltán Kovács: Proceedings 14th International Conference on Automated Deduction in Geometry (ADG 2023), Belgrade, Serbia, 20-22th September 2023, Electronic Proceedings in Theoretical Computer Science 398, pp. 43–52.; Presentation at
ADG 2023.
- Z. K., Bernard Parisse, Tomás Recio, M. Pilar Vélez, Jonathan H. Yu:
ShowProof in GeoGebra Discovery: Towards automated ranking of elementary geometry theorems.
Software Presentation at ISSAC 2024.
It is wonderful news that our software presentation won the
Distinguished Software Demonstration Award
this year at ISSAC.
Here are some on-going work and further ideas as next steps to continue this project:
- Soma Bartha and András Kerekes were involved in testing GeoGebra
Discovery's
ShowProof
command
in the frame of a GeoGebra internship this summer. We have a database of more than 25 geometry
statements from high school lecture notes, collected by their mathematics teachers
János Schultz and
János Mike, during several years of teaching experience at
Radnóti Miklós Secondary School in Szeged, Hungary. The test cases are named with
SB-*.ggb
in the test folders true and false
of GeoGebra's fork. An on-going work is to analyze these tests and give a detailed report for a Hungarian
journal in mathematics education.
- András implemented the GeoGebra files from the above mentioned database in Java Geometry Expert (JGEX). His analysis on the results will be added to the Hungarian report.
- We are hoping that there is some correlation between the algebraic difficulty and the geometric complexity of these statements.
A manual comparison by computing statistical correlation between the outputs of GeoGebra Discovery's algebraic difficulty degree and
the outputs of JGEX (the number of used derivation steps in the GDD method) could be an interesting further step.
András already collected not just the derivation steps but the height of the GDD derivation tree (among other information).
Computing the correlation for the above database is another step for the project.
- Since we have a larger database of more than 300 statements, it would be interesting to obtain the above statistics automatically,
without the requirement to construct each GeoGebra file manually in Java Geometry Expert. Therefore, a full version of the
GGB importer in JGEX would be a mandatory step. This requires some Java programming in DrawProcess.java, by implementing all missing GeoGebra
commands. This subproject will require several days of work, but it should be more or less straightforward if someone starts it with
some intermediate Java programming skills. Please let me know if you are interested in this.
- A different kind of programming task is to extend the
ShowProof
command to accept a second parameter. It is usually
a good idea to have an updated construction with equations and labels that contain the corresponding formulas.
But sometimes the user does not want that. In such cases, it would be useful to avoid updating the construction and leave it as is.
This subproject has already been started by Jonathan Yu.
- Jonathan also did some preliminary programming to have full cover off all the 300+ statements by exact descriptions
for each variables that require auxiliary definitions. These are called variable Botana variable descriptions.
After having a list of the missing descriptions, someone should finalize this part of the program. Also, a double-check of
all automatically created
ShowProof
outputs would be beneficial for the project.
- There are promising improvements in the output of GDD's GraphViz output. This is on-going work with András
and Alexander Vujic, a master student at PHDL, Linz, Austria.
A possible export of the GDD proof tree for JGEX's example 15
- Yet another project for a Hungarian journal: To give a full analysis on the Pete-Dőtsch theorem, by using
the
ShowProof
command. It is unclear if this should be a part of the work with Soma and András, or maybe
I will write that paper as extra work.
Entries on topic GeoGebra
- I restart my blog… (28 September 2020)
- A new GeoGebra version with better angle bisectors… (29 September 2020)
- Better language support… (6 October 2020)
- Detection of perpendicular lines… (19 October 2020)
- Points attached to an algebraic curve… (31 October 2020)
- Explore envelopes easily! (11 November 2020)
- Offsets of a trifolium (17 November 2020)
- Ellipsograph of Archimedes as a simple LEGO construction (18 November 2020)
- Pete-Dőtsch theorem (29 December 2020)
- Comparison improvements (25 January 2021)
- ApplyMap (26 January 2021)
- Discovering geometric inequalities (27 October 2021)
- Proving inequalities (28 October 2021)
- Supporting logic in function calculus (2 November 2021)
- Supporting logic with technology: Part 2 (12 February 2022)
- Difficulty of geometry statements (30 July 2024)
|
Zoltán Kovács
Linz School of Education
Johannes Kepler University
Altenberger Strasse 69
A-4040 Linz
|