Research And Implementation Of Euclidean Axiom System Based On Drools

With the rapid development of technology in recent years,artificial intelligence and intelligent education have become a popular research hotspot.Artificial intelligence is having a close connection to people in education,meanwhile changing people's basic necessities of life.It will break the barrier in getting knowledge and improving the fairness of education and make learning more interesting if we combine the AI technology with mechanical theorem-proving.Therefore it's necessary to research applying AI technology to the ereas of automated reasoning and automated theorem proving.The purpose of this thesis is to establish a system which can automatically solve and prove questions of Geometry problems,combing Euclidean axiom,Drools reasoning engine and AI technology.The main research of this thesis is as follows:1 ? Mathematical knowledge representation.we use the first-order predicate method to express the knowledge and use drl file for formalizing the axiom,based on the feature of knowledge in geometry.So knowledge in the field of human geometry can be transform to the a form which computers can express and computers can solving the Geometry problems in a right logical way.It achieves the goal of knowledge extraction in Geometry problems.2?Research and build of reasoning engine.this paper studies and designs the structure of the reasoning engine and make some design of related algorithm,we finally construct a reasoning system with correct logic and high quality performance.This reasoning engine can stimulate the corresponding rules to update the knowledge fact automatically.rules and facts are combined to obtain correct reasoning results.We also make a research on how to use mathematics computing symbolic engine to improve the efficiency of the system.3?Reasearch of rules priority dynamic forecasting algorithm.Its very import to revolve the conflicts when the conflicts of rules appear because its make a better way for reasoning.This paper makes a description of the state of the reasoning system.the system can dynamically change the rule priority according to the reasoning system running states,so that the performance of the reasoning system can be greatly improved.Combined with related theories and the main research content of this paper,An Euclid axiom reasoning system that can automatically solve Geometry problems is designed and realized.It's proves that this system can successfully solve basic geometric problems according the result of different types of geometric problems tests.This provides a new idea for automatic problem solving.