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

摘要

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. A set of metrics for measuring interestingness of theorems in automated theorem finding by forward reasoning have been proposed, and case studies to measure interestingness of the theorems of NBG set theory and Peano's arithmetic were performed. This paper presents a case study in Tarski's geometry to show the generality of proposed metrics. In the case study, we use the metrics to measure interestingness of the theorems of Tarski's geometry obtained by using forward reasoning approach, and confirm the effectiveness of the metrics.