Set Theory Equation Type Theorem Proving Systems Research And Development

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 first-order 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 human-readable 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 human-readable 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 depth-first 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 human-like 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.