Finding Theorems in NBG Set Theory by Automated Forward Deduction Based on Strong Relevant Logic

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. For the problem, Cheng has proposed a forward deduction approach based on strong relevant logic. To verify the effectiveness of the approach, we tried to rediscover already known theorems in NBG set theory by using the approach, and succeeded in rediscovery of several known theorems. However, the method of the rediscovery is ad hoc, but not systematic. This paper gives an analysis and discussion for our experiment method and results from the viewpoint of the systematic method. The paper also presents some issues and future research directions for a systematic method of automated theorem finding based on Cheng’s approach.