Unifying the prover in GeoGebra—and speeding it up
During the last months there was a remarkable work done on adding publicity for GeoGebra's Automated Reasoning Tools. In a nutshell, GeoGebra's Automated Reasoning Tools can investigate and even prove theorems in planar Euclidean geometry. Not everything is managable, but most statements of the secondary school topics are doable quite quickly, that is, in one or two seconds at most for each.
So we agreed on removing one of the algorithms, and we designated the one used by the Prove command. That piece of tricky algorithm was programmed in Giac, the built-in computer algebra system in GeoGebra, to make it possible to perform the computations quickly enough, even if Giac's capabilities on computing Gröbner bases are just limited. The algorithm we used (see page 27 in a former presentation) in the Prove command was a simple trick, namely, to add some sophisticated preliminary conditions to the list of hypotheses, for instance, that all freely defined triangles in the construction are non-degenerate. These preconditions can avoid further investigation of the so-called non-degeneracy conditions in the output.
Now, after a few months of silence I finally removed that tricky algorithm from GeoGebra. The Gröbner bases computations in Giac are already so mature that we do not need those tricks any longer. Also, I learned that speed is more important that a precise list of degeneracy conditions. Thus the number of fix coordinates have been automatically set to 4 in the ProveDetails algorithm.
To make the long story short, I simply provide here two outputs of the daily run of our benchmarking system. The old results show how different methods solve the test problems, here the last four columns are interesting, the numbers 235 and 205 are produced by Singular, an external reference CAS application, for the Prove and the ProveDetails commands, respectively:
and the values 158 and 209 were done by Giac, also for the Prove and ProveDetails commands. After the removal the new ones for the last two columns are these values:
This clearly shows that the Prove and ProveDetails commands are now unified and have a much better performance. Actually there is no significant difference in speed between Singular and Giac any more. (Actually the former number 205 in Singular/ProveDetails is 224 by now.)
These numbers are used in GeoGebra Classic 5 which is the reference version of the prover. (The value on the top is the number of test cases that were successful, and the value at the bottom is a "final goodness value" that expresses speed as well.) The same numbers are also available for the web version, too: the former values were 151/184 and now they are 208/209 (the difference can be because of some other issues).
The unification and speedup result in an about twice quicker performance of the Relation Tool as well when a symbolic check is requested. Also, some nice complicated theorems can be proven now without any difficulties, for example, Napoleon's theorem:
Interestingly enough, this theorem is true just on parts.
The changes described above will be publicly available in GeoGebra 5.0.519.0, hopefully in the first half of January 2019.
The project was initiated by Tomás Recio in 2010, and programmed by a few people including me as well. The final paper on the educational benefits of the developments was published in the International Journal for Technology in Mathematics Education in the number April-June 2018 (Volume 25 Number 2). A preliminary version of that paper was already available as a GitHub project.
This disseminating work was mostly performed by Tomás Recio, M. Pilar Vélez and me and took a few months. After several discussions we finally faced a complicated communication issue, namely, that the commands Prove and ProveDetails use different algorithms in the background, and this fact results confusing differences sometimes in the normal use of the program. Also, the Relation Tool initiates two computations via these different commands to have a more detailed understanding if a statement is true or not. In the very internals of the program this is handled cleverly, that is, normal users should not be confused because of that, but this issue makes the debugging and the manual verification of the methods rather difficult.So we agreed on removing one of the algorithms, and we designated the one used by the Prove command. That piece of tricky algorithm was programmed in Giac, the built-in computer algebra system in GeoGebra, to make it possible to perform the computations quickly enough, even if Giac's capabilities on computing Gröbner bases are just limited. The algorithm we used (see page 27 in a former presentation) in the Prove command was a simple trick, namely, to add some sophisticated preliminary conditions to the list of hypotheses, for instance, that all freely defined triangles in the construction are non-degenerate. These preconditions can avoid further investigation of the so-called non-degeneracy conditions in the output.
Now, after a few months of silence I finally removed that tricky algorithm from GeoGebra. The Gröbner bases computations in Giac are already so mature that we do not need those tricks any longer. Also, I learned that speed is more important that a precise list of degeneracy conditions. Thus the number of fix coordinates have been automatically set to 4 in the ProveDetails algorithm.
To make the long story short, I simply provide here two outputs of the daily run of our benchmarking system. The old results show how different methods solve the test problems, here the last four columns are interesting, the numbers 235 and 205 are produced by Singular, an external reference CAS application, for the Prove and the ProveDetails commands, respectively:
These numbers are used in GeoGebra Classic 5 which is the reference version of the prover. (The value on the top is the number of test cases that were successful, and the value at the bottom is a "final goodness value" that expresses speed as well.) The same numbers are also available for the web version, too: the former values were 151/184 and now they are 208/209 (the difference can be because of some other issues).
The unification and speedup result in an about twice quicker performance of the Relation Tool as well when a symbolic check is requested. Also, some nice complicated theorems can be proven now without any difficulties, for example, Napoleon's theorem:
The changes described above will be publicly available in GeoGebra 5.0.519.0, hopefully in the first half of January 2019.
Comments