Title
A systematic methodology for automated theorem finding.
Abstract
The problem of automated theorem finding is one of the 33 basic research problems in automated reasoning which was originally proposed by Wos in 1988, and it is still an open problem. To solve the problem, an approach of forward deduction based on the strong relevant logics was proposed. Following the approach, this paper presents a systematic methodology for automated theorem finding. To show the effectiveness of our methodology, the paper presents two case studies, one is automated theorem finding in NBG set theory and the other is automated theorem finding in Peano's arithmetic. Some known theorems have been found in our case studies.
Year
DOI
Venue
2014
10.1016/j.tcs.2014.06.028
Theoretical Computer Science
Keywords
DocType
Volume
Automated theorem finding,Forward deduction,Strong relevant logic,NBG set theory,Peano's arithmetic
Journal
554
Issue
ISSN
Citations 
C
0304-3975
11
PageRank 
References 
Authors
0.92
5
3
Name
Order
Citations
PageRank
Hongbiao Gao1237.06
Yuichi Goto212622.31
Jingde Cheng354285.38