The Geometric Proof System Based On Mobile Internet Research And Implementation

Geometry theorem proving system is a kind of powerful geometric CAI(ComputerAided Instruction, CAI) which has a pivotal position in geometry education application.At present, there are many successful geometry theorem proving systems, such asMathXP, Z+Z Intelligent Education Platform and Geometry Explorer. Because ofrunning on top of the traditional PC, they are unable to meet the usage requirements ofanytime and anywhere.With the development of Mobile Internet, the reductions in price and theimproving in processing capacity of portable smart device, that realizing a geometrytheorem proving system for portable smart device becomes possible. Based on theresearch of automated theorem proving, combining the construct-input method ofgeometric proposition, this paper devoted to realizing a Mobile-Internet-Basedgeometry theorem proving system using the current popular mobile developmenttechniques. The main works of this paper are:1. Study the description and input methods of geometric proposition. Describes thepredicate description method of geometric proposition using first-order logic, andintroduces predicate-input and construct-input method of geometric proposition. On thebasis of analysis and study of the two input methods, combined with the object-orienteddesign ideas, we propose an object-oriented construct-input method for formalproposition.2. Study automated theorem proving, explore the methods of combining automatedtheorem proving and mobile internet. Study rule-based forward search method forgeometry theorem proving, analyze the realization of theorem proving system, andrealize the combination of theorem proving system and the mobile internet.3. Design and implement a Mobile-Internet-based geometry theorem provingsystem. Provide an exhaustive introduction of system design and implementation inrequirement analysis, overall design, detailed design and implementation.The system referred in this paper combines automated theorem proving and theMobile Internet, provides a mobile learning environment of geometry, breaks the limitations of the equipment, and meets usage requirements well.