Geometric Theorem Proving - GUI

This page collects ideas for the changes in the GUI which will be necessary to integrate the theorem prover. For more information about geometric theorem proving look on the according ​wiki-page.

Algebra View

The boolean value for the tested theorem should have one of the following values:

If it was tested numerically (without the prover):

• true
• false

If it was tested with the prover:

• always true
• always false

• generally true
• generally false

Always true means that this theorem always holds (without any additional non degeneration conditions), generally true means that the theorem is true if some non degeneration conditions hold.

In case the answer is generally true or generally false the non degeneration conditions can be displayed by choosing the according item on the right-click drop-down list of the boolean.

If the prover cannot give the answer (due to timeout or it detects that the problem will be too difficult to solve in a reasonable time), then as a fallback, the numerical test will be run automatically.

Object Properties

In the Object Properties of such an boolean value there should be an option whether to use the prover or the standard numerical method. At the beginning this should be set to numeric by default.

Settings (Options/Settings)

Here should be some options (maybe in the advanced tab) for

• the timeout of the prover,
• if a boolean expression should be automatically evaluated by a prover,
• (later) additional options for the prover (e.g. suggested method).