Integrating OpenGeoProver into GeoGebra

What has to be sent from GeoGebra (GG) to OpenGeoProver (OGP)?

• The construction (a list of all constructions)
• The statements
• The parameters
  • Prover method (only Wu's method is implemented now, Groebner basis method will follow and maybe others in future)
  • Output format (specifying how much should be returned: only true/false, the ndg-conditions or the whole prove)
  • Time limit
  • Space limit (maximal number of terms in single polynomial obtained during proving process)

What has to be returned from OGP to GG?

That depends on the output format parameter. At least a Boolean value telling if the theorem is true or false.

How should the construction and the statement be sent to OGP and how should OGP return the ndg-conditions?

The preferred format is xml since both GG and OGP understand xml (but have different formats). It is slower than translating the construction of GG into one of OGP directly but is significantly easier to implement and keeps both projects independent.

How can one use the prover in GG?

For the beginning there will be some commands for statements like IsIdentical, IsParallel, IsPerpendicular, IsCollinear, ...
This commands will NOT use numerical methods but only symbolical.
There will be numerical methods too, which will have names like IsIdenticalNumeric, IsParallelNumeric, etc. to make the user clear that these commands do not work exactly.

The parameters for the prover should be added to a new tab in Options/Settings.

Ideas for future developments:

• A proper prover window where one can choose what to prove by drop-down lists.
• A possibility to show how the construction would look like when the ndg-conditions are fulfilled.