OpenGeoProver debuting

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.

Related Posts

  • 19 and makes theorems proven Back again in Austria; I've been to two additional conferences during the last two weeks. The first one, in Serbia, was about computer aided mathematics education, and the second one was […]
  • Theorem proving Well, I forgot my own introduction in the first post, but maybe it is more important for me that I work in a great team. Balazs already wrote a few words about himself; I am also a […]
  • Be intuitive Days are passing and the summer conference time is getting closer and closer. In two weeks we (Simon and I) will attend EACA 2012 in Spain, and then CADGME 2012 in Serbia. For both we are […]
  • Google Summer of Code Mentor Summit Thanks to Google, this year we had 7 students for the Google Summer of Code program. This was the 3rd year we have been involved after 5 and 7 supported students since 2010. As an official […]
  • 4.2 Release Candidate GeoGebra 4.2 will be released soon. 21 developers have contributed to this release, so there are many new and exciting features to explore and enjoy! Here are some of the things you can […]
Posted in Community, Development, GGB Tagged with: , , , , ,
One comment on “OpenGeoProver debuting
  1. 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.)


About GeoGebra

GeoGebra is free and multi-platform dynamic mathematics software for all levels of education that joins geometry, algebra, tables, graphing, statistics and calculus in one easy-to-use package. It has received several educational software awards in Europe and the USA.

Quick Facts

  • Graphics, algebra and tables are connected and fully dynamic
  • Easy-to-use interface, yet many powerful features
  • Authoring tool to create interactive learning materials as web pages
  • Available in many languages for our millions of users around the world
  • Free and open source software
© 2020 International GeoGebra Institute