Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Open Source Prover in the Attic

Zoltán Kovács, Alexander Vujic

TL;DR

Open-source JGEX presents a case study on extending a large automated geometry prover without the original authors. The authors evaluate practical paths including language translations, user interface modernization, and updated mathematical methods (Gröbner basis and Wu's method), along with bug fixes and visualization improvements. They document real-world challenges such as incomplete translation keys, Java-version compatibility, and code-quality issues, proposing concrete engineering solutions like a CSV-based translation system, GraphViz visualization, and web deployment. The work demonstrates that saving and evolving legacy automated reasoning tools is feasible and valuable for education, communities, and future tooling.

Abstract

The well known JGEX program became open source a few years ago, but seemingly, further development of the program can only be done without the original authors. In our project, we are looking at whether it is possible to continue such a large project as a newcomer without the involvement of the original authors. Is there a way to internationalize, fix bugs, improve the code base, add new features? In other words, to save a relic found in the attic and polish it into a useful everyday tool.

Open Source Prover in the Attic

TL;DR

Open-source JGEX presents a case study on extending a large automated geometry prover without the original authors. The authors evaluate practical paths including language translations, user interface modernization, and updated mathematical methods (Gröbner basis and Wu's method), along with bug fixes and visualization improvements. They document real-world challenges such as incomplete translation keys, Java-version compatibility, and code-quality issues, proposing concrete engineering solutions like a CSV-based translation system, GraphViz visualization, and web deployment. The work demonstrates that saving and evolving legacy automated reasoning tools is feasible and valuable for education, communities, and future tooling.

Abstract

The well known JGEX program became open source a few years ago, but seemingly, further development of the program can only be done without the original authors. In our project, we are looking at whether it is possible to continue such a large project as a newcomer without the involvement of the original authors. Is there a way to internationalize, fix bugs, improve the code base, add new features? In other words, to save a relic found in the attic and polish it into a useful everyday tool.
Paper Structure (8 sections, 4 figures)

This paper contains 8 sections, 4 figures.

Table of Contents

  1. Introduction
  2. Expectations
  3. Translations
  4. Modern Interface
  5. State-of-the-art Mathematics
  6. Fixing Bugs and Adding Improvements
  7. Conclusion
  8. Acknowledgments

Figures (4)

  • Figure 1: JGEX proves a part of the nine-point theorem by using the GDD method. Its user interface is set to German.
  • Figure 2: The output of the GDD method is visualized as a tree.
  • Figure 3: The GDD method finds a proof that is not a tree. The interface is set to German and the connecting edges of the graph are not shown.
  • Figure 4: A better visualization of the GDD proof by using GraphViz.