Measuring Interestingness of Theorems in Automated Theorem Finding by Forward Reasoning Based on Strong Relevant Logic
- Resource Type
- Conference
- Authors
- Gao, Hongbiao; Li, Jianbin; Cheng, Jingde
- Source
- 2019 IEEE International Conference on Energy Internet (ICEI) Energy Internet (ICEI), 2019 IEEE International Conference on. :356-361 May, 2019
- Subject
- Communication, Networking and Broadcast Technologies
Computing and Processing
Power, Energy and Industry Applications
Cognition
Geometry
Measurement
Set theory
Power systems
Systematics
Conferences
Metric
automated theorem finding
forward reasoning
strong relevant logic
Tarski's Geometry
- Language
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.