A Set of Metrics for Measuring Interestingness of Theorems in Automated Theorem Finding by Forward Reasoning: 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. The problem implicitly requires some metrics to be used for measuring interestingness of found theorems. However, no one addresses that requirement until now. This paper proposes the first set of metrics for measuring interestingness of theorems. The paper also presents a case study in NBG set theory, in which we use the proposed metrics to measure the interestingness of the theorems of NBG set theory obtained by using forward reasoning approach and confirms the effectiveness of the metrics.