Measuring Interestingness of Theorems in Automated Theorem Finding by Forward Reasoning: A Case Study in Peano's Arithmetic

摘要

Wos proposed 33 basic research problems for automated reasoning field, one of them is the problem of automated theorem finding. The problem has not been solved until now. The problem implicitly requires some metrics to be used for measuring interestingness of found theorems. We have proposed some metrics to measure interestingness of theorems found by using forward reasoning approach. We have measured interestingness of the theorems of NBG set theory by using those metrics. To confirm the generality of the proposed metrics, we have to apply them in other mathematical fields. This paper presents a case study in Peano's arithmetic to show the generality of proposed metrics. We evaluate the interestingness of theorems of Peano's arithmetic obtained by using forward reasoning approach, and confirm the effectiveness of the metrics.