The Research Of The Automatic Verification Of The Answers Of Elementary Algebra Proying

Educational informationization is an important step to achieve the modernization of education, and it is the important content and the main symbol of the modernization of education. Mathematics is both a basic subjects and a thinking field which play a very important role in teaching to cultivate students' thinking skills, computing skills, imagination and practical ability and creative ability. The mathematical proving is an important part of mathematics teaching. It serves an irreplaceable role of other ways in training and assessment. How to use modern information technology in the teaching of mathematical proof to implement the formal analysis and verification of mathematical proof has been more and more attention. In middle school mathematics teaching, elementary algebra is the basis of learning plane geometry, solid geometry, trigonometric functions, analytic geometry and calculus. How to automatically assess the answers to subjective questions, especially those to proving exercises in elementary algebra, is a problem to be solved in theory and practice and it has wide application prospects. In this paper, we focus on the mathematical proof as answers of proving exercises in algebra. We analyze mathematical proof language characteristics, design a system of fragments of natural language and obtain the formal semantics of a mathematical proof through a dynamic analysis method on the basis of discourse representation theory and then verify it in a theorem proving system to make sure whether the original mathematical proof is correct. The study in this paper involves disciplines of linguistics, logic, computational science and mathematics and consists of the following parts.(1) The characteristics of the language of mathematical proofsMathematical proof language is the language through which we write the answers of the proving exercises what we are addressing. This language has a semi-formal characteristic, which means it is a natural language mixed with mathematical formula. This paper analysis of its basic characteristics from the two aspects of mathematics and language (2) The syntax of the language of mathematical proofsFrom Montague's famous PTQ, we tend to construct fragments of natural language to study formal semantics. for example, generalized quantifier theory, situation semantics, discourse representation theory, the type of logical syntax. This paper constructs a fragment of the language of mathematical proofs which can meet the the basic requirements of mathematical proofs.(3) The semantcis of the language of mathematical proofsDiscourse representation theory is the first one of dynamic semantic theories. It extends the analysis object from single sentence to a series of sentences, reflecting the anaphora between a noun and its antecedent. This paper extends the constructing rules and the discourse representation structure of discourse representation theory to enable it to meet the need for analyzing mathematical proofs.(4) The automated verification method of mathematical proofsMachine theorem proving is a method to prove mathematical theorems through a machine and it is a study filed of artificial intelligence. This paper studies the method to translate the DRS of mathematical proofs to the formal proofs of Isabelle, and design automatic tactics to verify the proofs in Isabelle, and analyze the ability of the calculation based on tactics.