Automated Theorem Finding by Forward Reasoning Based on Strong Relevant Logic : Methodology and Case Studies
宏彪 高 · Institutional Repositories DataBase (IRDB) · 2015
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. The problem of automated theorem finding is "What properties can be identified to permit an automated reasoning program to find new and interesting theorems, as opposed to proving conjectured theorems?". The most important and difficult requirement of the problem is that, in contrast to proving conjectured theorems supplied by the user, it asks for the criteria that an automated reasoning program can use to find some theorems in a field that must be evaluated by theorists of the field as new and interesting theorems. The significance of solving the problem is obvious because an automated reasoning program satisfying the requirement can provide great assistance for scientists in various fields. The problem of automated theorem finding is still an open problem. Although there have been valuable works on the research of automated theorem proving, those works cannot be applied to the problem of automated theorem finding. On the other hand, a few works aimed to automated theorem discovery and automated theorem generation have been done. However, the problem of automated theorem finding which is to pursue properties to find new and interesting theorems is different from the automated theorem discovery and automated theorem generation. In fact, Wos's problem can be regarded as an attempt to find a systematic methodology in automated reasoning area, but the works on automated theorem discovery and automated theorem generation are not. The works on automated theorem discovery and automated theorem generation almost aimed to one certain mathematical field and current results of those works are only rediscovery of some simple known theorems in some certain fields, rather than finding new and interesting theorems. Cheng proposed that forward reasoning based on strong relevant logic is a hopeful approach to solve the automated theorem finding problem. Reasoning is the process of drawing new conclusions from some premises which are already known facts and/or previously assumed hypotheses. Because reasoning is the only way to draw new, previously unknown conclusions from given premises, there is no discovery process that does not invoke reasoning. On the other hand, by using strong relevant logic as the fundamental logic to underlie reasoning for automated theorem finding, one can avoid paradoxical theorems in using classical mathematical logic, various conservative extensions of classical mathematical logic, and traditional relevant logics. However, no one showed how to use a systematic method by forward reasoning based on strong relevant logic to do automated theorem finding. This thesis proposed a systematic methodology for automated theorem finding by forward reasoning based on strong relevant logic. The methodology consists of five phases. The first phase is to prepare logical fragments of strong relevant logic for various empirical theories. The second phase is to prepare empirical premises of a target empirical theory. The third phase is to reason out empirical theorems in the target empirical theory. The fourth phase is to abstract these empirical theorems. The fifth phase is to find interesting theorems from the empirical theorems. The methodology holds generality so that we can use it to do automated theorem finding in various fields. In order to show the effectiveness of our methodology, we did three case studies of automated theorem finding in three different mathematical fields by using our methodology. The first mathematical field is NBG set theory, the second one is Peano's arithmetic and the third one is graph theory. For each case study, we elaborated how to apply our methodology, showed the results and gave an evaluation. After we presented three case studies, we evaluated the methodology from viewpoint of generality. This work has following contributions. The first contribution is that we proposed a systematic methodology for automated theorem finding based on the semi-lattice of formal theories in which the core is strong relevant logic, and the minimum element is the formal theory of axiomatic set theory, above it other formal theories can be established like number theory, graph theory, and lattice theory, so the methodology holds generality for various mathematical fields. The second contribution is that we proposed a method to do automated theorem finding based on the abstraction process of mathematical concept such that we can systematically find theorems from simple theorems to complex theorems. The third contribution is that we proposed a method to generate hypothesis by using forward reasoning approach by strong relevant logic and then combine automated theorem proving approach to systematically find those theorems proved by mathematical induction. The fourth contribution is that we performed three case studies of automated theorem finding in three different mathematical fields by using our methodology and clearly showed our method and results. Before our works, it is only in theory to use forward reasoning approach based on strong relevant logic to perform automated theorem finding in different mathematical fields, but our works showed the detail and systematic procedure of automated theorem finding clearly. This thesis is organized as follows. Chapter 1 presents the background and purpose of this research. Chapter 2 explains the basis of the strong relevant logic and the terminology of automated theorem finding. Chapter 3 presents our systematic methodology for automated theorem finding. Chapter 4 presents the case study of preparation of logical fragments. Chapter 5 presents the case study of automated theorem finding in NBG set theory. Chapter 6 presents the case study of automated theorem finding in Peano's arithmetic. Chapter 7 presents the case study of automated theorem finding in graph theory. Chapter 8 gives a discussion about our methodology. Finally, concluding remarks are given in Chapter 9.