Measuring Interestingness of Theorems in Automated Theorem Finding by Forward Reasoning Based on Strong Relevant Logic

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 based on strong relevant logic have been proposed, and a case study to measure interestingness of the theorems of Tarski's geometry was performed. The result of the case study showed that the proposed metrics were hopeful for measuring interestingness of theorems in automated theorem finding. However, there is no research about the influence of different logical fragments of strong relevant logic on theorem finding. This paper presents a case study to measure interestingness of theorems obtained by using forward reasoning based on different logical fragments. The result shows that different logical fragments have different effects on the four factors of interestingness of theorems.