Ivan Petrović, PhD student at University of Belgrade
The EACA conference has just ended, but the hard development in theorem proving did not stop. Our Serbian contributor Ivan Petrović did very nice improvements on GeoGebra by working hard on the OpenGeoProver (OGP) prototype during the last week. Now the desktop version of GeoGebra has 5 possible ways to prove a statement, and OGP, the latest one, does a really good job.
Predrag Janičić, associate professor at University of Belgrade
Now the recent benchmarks show that Ivan’s prover (based on Predrag Janičić‘s GCLC, but fully rewritten in Java) gives the correct answer in 40 out of the 44 test cases, and beats the other provers in the most difficult computations, namely the Desargues’s theorem and the Simson line. In general, it has the second best average in computation time (Recio: 89, OGP: 315, Botana: 540, PureSymbolic: 2091 ms), and the best standard deviation (OGP: 250, Recio: 399, Botana: 2226, PureSymbolic: 9467 ms), which means OGP is the most stable prover engine for GeoGebra at the moment. (The 5th prover is the Auto method: it tries to find the best prover engine by using some heuristics. This is the default in GeoGebra.)
The official announcement of our joint work will be on 22 June at the CADGME conference in Novi Sad, Serbia.
It is also important to mention that OGP has a very small footprint. The JNLP packed versions (which can be used in applets on a web page, i.e. also in GeoGebraTube) are between 55 and 70 kilobytes. (Normally, the original.jar file is about 500 kilobytes when only the.class files are included.)