Set Theory Equation Type Theorem Proving Systems Research And Development  Posted on:20070904  Degree:Master  Type:Thesis  Country:China  Candidate:X L Tang  Full Text:PDF  GTID:2208360182457556  Subject:Software engineering  Abstract/Summary:  PDF Full Text Request  There has been a lot of success in the study of automated theorem proving during the past 50 years. The most prominent approaches in this area include firstorder theorem proving in logic made by Newell, Shaw, Simon and Robinson in 1960's, automated theorem proving in elementary geometry made by Wu Wentsun, Zhang Jingzhong and Yang Lu. In particularly, Zhang Jingzhong's method can give results in humanreadable format, which makes it more applicable in CAI(Computer Aided Instruction) software designing. In this paper we present an approach to the machine proof of theorems in set theory. Though it is well known that proof of theorems in set theory can be interpreted to simplification of certain equation system in Boolean algebra, there is no report found in the literature on the humanreadable yet. The reasoning functions concerning the set theory are also relatively weak in many widely used mathematical software like Maple, Mathematica and Matlab. The contribution of this paper could be summarized as follows:(1) Improved the iterated deepening depthfirst search algorithm to speed up the searching routine in machine proof for theorems in set theory;(2) Integrated a few heurestic rules based on the human expert experience in the search algorithm;(3) Implemented the algorithm by using of the Lisp programming language;(4) Discussed some techniques in debug and trace for the implementation;(5) Designed a data format to produce detail explanation in each step of reasoning;(6) Constructed a theorem classification modular which can process common knowledge in humanlike way.In the final, the author also discussed the further methods that can complement the algorithm: increase the agility in searching strategy, add the machine learning function and investigate the dynamic adjustment of the rule base and search order.  Keywords/Search Tags:  artificial intelligence, automated theorem proving, mathematics mechanization, set theory, readable proof  PDF Full Text Request  Related items 
 
