Automated theorem finding by forward deduction based on strong relevant logic: A case study in NBG set theory

The problem of automated theorem finding is one of 33 basic research problems in automated reasoning which was originally proposed by Wos in 1988, and it is still an open problem. To solve the problem, a forward deduction approach based on the strong relevant logics was proposed. To verify the effectiveness of the approach, this paper presents a case study of automated theorem finding in NBG set theory by forward deduction based on the strong relevant logics. The ultimate goal of automated theorem finding in NBG set theory is to find new and interesting theorems. As the first step, this case study tries to do “rediscovery” in NBG set theory, i.e., to deduce already proved theorems from axioms, definitions and /or other theorems of NBG set theory. However, from the viewpoint of the mechanism of deducing theorems, “re-discovery” is as same as “discovery”. The paper shows several known theorems rediscovered successfully by the approach. The paper also shows issues of the approach for real “discovery”.