Generally, for a relatively complicated human proof, a substantial amount of work and imagination
is needed for converting it into a visually dynamic representation of the proof. It is much harder to
develop a general tool so that the creation of visual presentations can be done easily. This tool has
been implemented in JGEX.
In JGEX, a complete proof created manually consists of three parts: The given part (the hypotheses), the to prove part (the conclusion) and the proof part. See appendix for detail description.
The first part is the hypotheses in construction form. To input the hypotheses, the user can just draw
on the diagram pane and the hypotheses will be generated accordingly and automatically. Then the
user gives the keywords "To prove" to indicate the inputting of conclusion. After the conclusion
the user can write the proof part with any proof method, mainly with mouse clicks.
The unique traits of the method is that it mainly uses mouse clicks and uses keyboard strokes only
when they are necessary or convenient, e.g., some annotations or geometry statements in English.
With mouse clicks, it is not only easy and intuitive to use, but is also less error-prone. For example,
instead of typing “tirangle DAG”, we can use the mouse to click points D, A, and G in the diagram
to generate the text “tirangleDAG”. Thus there is no error: the order of the points in the text and the
orientation of the triangle in the diagram are preserved. Furthermore, with the equilateral triangle
icon, we can click any two points to drag an equilateral triangle in the diagram, and at the same
time the text, say “equilateral tirangle ABC”, is automatically generated.
JGEX Help