Introduction to Manually Input Method.


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.

 

Layout of the Proof

JGEX Help