Font Size: a A A

Research On Visually Dynamic Presentation Of Proofs In Plane Geometry

Posted on:2011-12-15Degree:DoctorType:Dissertation
Country:ChinaCandidate:Z YeFull Text:PDF
GTID:1118330332478380Subject:Computer application technology
Abstract/Summary:PDF Full Text Request
When we read a proof in a geometry book, we often need to spend time and energy on identifying a geometry element in the proof text with that in the corresponding diagram. When the diagram becomes complicated, the problem could turn to be more serious. It is helpful to develop methods to generate and present proofs so that they can be read and understood easily, which is also the main research subject of proof visualization.This thesis makes thorough study of the existing problems in proof visu-alization. The essential techniques include dynamic geometry, the generation, organization and visualization of readable geometry proofs. The main purpose of this research is to develop effective methods to generate and visualize geome-try proofs, and to help the reader to understand these proofs. The main research contents include following topics:1. Design special and effective methods for solving constraints of geometry diagrams. Geometry diagrams play a very important role in geometry proving. Being given a geometry theorem, it can be considered as a pro-cess of constraint solving to generate the corresponding diagram and do transformation to the diagram. Traditional methods do not translate ge-ometry constraints into unified representations, so they have many prob-lems, especially on the efficiency and stability. This research try to develop an efficient algorithm to do constraint solving for geometry diagrams. The basic idea is that, by taking the advantage of some special properties of geometry theorems, we use powerful algebraic methods to do geometry constraint solving.2. Study the techniques for inputting and visualizing geometry proofs. The interrelationship between geometry proof text and the corresponding ge-ometry elements in the diagram is the key to proof visualization. For tradi-tional geometry proofs in geometry text books, the two are separated. The user needs to identify them himself when he is reading the proofs. In this research, we study the organization of traditional geometry proofs, hop-ing that we can propose a formal structure for the proofs. And based on this formal structure, we hope that we can propose a method to visualize geometry proofs. Besides, this research investigates several different methods for proof gen-eration. On one hand, we develop a graphical interface with which the proofs can be input manually. On the other hand, we offer an automated method, with which the user needs only to input the hypotheses of the geometry theorem and then the proof will be generated automatically.3. Study the methods for automated generation of readable proofs and for organizing proofs hierarchically. Geometry proofs are always required to be short so that they can be read and understood easily. Since the human brain can only remember several steps at one time, people are usually un-able to read and understand proofs with too many steps. Our purpose is to develop methods which will only show the main steps of the proofs, and hide the unnecessary steps at the same time. The hidden steps will only be shown when the user really needs. In this way, the user can grasp the key steps when reading the proofs.By investigating the above issues, this thesis obtain several important re-search results, the main contributions are listed below:1. Develop a new method based on geometry theorems in construction form for geometry constraint solving. For geometry theorems in construction form, we can assign the parameters to the points sequentially according to the order of points in the hypotheses. Then we can translate the geometry constraints into polynomial equations and triangulate them easily. With the polynomial equations after the triangulation, we can solve geometry constraints sequentially and effectively. The method has many advantages comparing to the traditional methods, for example, it is very stable and can generate many different cases for the diagram, and it can do reasoning and proving to the properties of the geometry diagram. 2. Propose a new kind of presentation for proofs in plane geometry:visually dynamic presentation of proofs or VDPP. We also propose a formal structure for the plane geometry proofs, and based on this structure, we develop a method with which the user can input VDPPs manually. The most dis-tinctive feature of VDPP is its interrelationship between proof text and the corresponding elements in the diagram. In the manually input method, the structure of the proof is strictly defined and the user can input the VDPPs mainly uses mouse clicks.3. Develop two methods for automated generation of VDPPs based on un-ordered geometry:the full angle method and the deductive database method. The two methods are all based on unordered geometry. The proofs in this geometry model are always short and easy to generate mechanically. More-over, combining the forward chaining with backward chaining, we develop a method for automated generation of geometry proofs with hierarchical structure. With this structure, the user can focus on the main steps, and when a specific step needs further investigation, he can expand the step for the detailed proofs. In the deductive database method, we generate a database which contains many facts of the diagram, and we have visual-ized the database successfully.4. With all the research results we have achieved, we develop a geometry system:Java Geometry Expert (JGEX). JGEX consists of three parts:the drawing part, the proving and reasoning part, and the part for proof pre-sentation. The most distinctive feature of JGEX is its method for presenting VDPPs. Also it has two methods for generating VDPPs:the manual input method and the automated method.Based on the methods we have developed, we have successfully created over two hundred VDPPs. These methods and examples can not only be used for geometry education in elementary schools, but also be used by people who are interested in plane geometry to study geometry proving.
Keywords/Search Tags:Dynamic Geometry Software, Automated Theorem Proving, Java Geometry Expert, Synthetic Proof, Visually Dynamic Presentation, of Proofs, The Full-Angle Method, The Deductive Database Method, JGEX
PDF Full Text Request
Related items