Automated Theorem Finding by Forward Deduction Based on the Semi-lattice Model of Formal Theory: 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, we tried to rediscover already known theorems in NBG set theory by using the approach, and succeeded in rediscovery of several known theorems. However, from the viewpoint of automated theorem finding, our method of the rediscovery is ad hoc, but not systematic. This paper proposes a systematic method based on the semi-lattice model of formal theory for deducing theorems and finding theorems which are two key phases of automated theorem finding. The paper presents a case study for automated theorem finding in NBG set theory and also shows some future research directions for automated theorem finding.