Automatic theorem proving in set theory

摘要

This paper describes a program which proves theorems in set theory by the use of heuristics. The use of methods which are analogous to human methods is its main characteristics. By splitting, a different theorem is first brokes into more easily proud parts. The heuristics for the following steps, which are the resuse of observation and imitation of the mathematics' methods, emphasize the use of many selections methods and the choice of suitable representations. In particular, a graph is constructed to represent binary relations. The program has been used to prove about 150 theorems in more and axiomatic set theory, sampling with functions, orderings, congruence relations and ordinal numbers.