Automated Theorem Finding by Forward Reasoning Based on Strong Relevant Logic : Methodology and Case Studies

• Material Type: 博士論文
• Title: Automated Theorem Finding by Forward Reasoning Based on Strong Relevant Logic : Methodology and Case Studies
• Author/Editor: 高, 宏彪
• Author Heading: 高, 宏彪
• Publication Date: 2015
• Publication Date (W3CDTF): 2015
• Alternative Title: 強相関論理に基づく前向き推論による自動定理発見 : 方法論と事例研究
• Periodical title: 博士論文（埼玉大学大学院理工学研究科（博士後期課程））
• Degree grantor/type: 埼玉大学
• Date Granted: 2015-03-24
• Date Granted (W3CDTF): 2015-03-24
• Dissertation Number: 甲第984号
• Degree Type: 博士(工学)
• Conferring No. (Dissertation): 甲第984号
• Text Language Code: eng
• Target Audience: 一般
• Note (General): type:text; 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.; Abstract iAcknowledgments iiiList of figures viList of tables vii1 Introduction 11.1 Background and motivation . . . . . . . . . . . . . . . . . . . . . . 11.2 Purpose and objectives . . . . . . . . . . . . . . . . . . . . . . . . . 31.3 Structure of the thesis . . . . . . . . . . . . . . . . . . . . . . . . . 32 Basic notions and notations 52.1 Logic-based reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . 52.2 Strong relevant logics . . . . . . . . . . . . . . . . . . . . . . . . . . 62.3 Forward deduction engine . . . . . . . . . . . . . . . . . . . . . . . 102.4 The semi-lattice model of formal theories . . . . . . . . . . . . . . . 113 A systematic methodology for automated theorem finding 133.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133.2 Systematic methodology . . . . . . . . . . . . . . . . . . . . . . . . 134 Preparation of logical fragments 215 Case study: Automated theorem finding in NBG set theory 245.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 245.2 Perform the methodology . . . . . . . . . . . . . . . . . . . . . . . 245.3 Case study for explicitly epistemic contraction by predicate abstracton 315.4 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 346 Case study: Automated theorem finding in Peano's arithmetic 366.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 366.2 Perform the methodology . . . . . . . . . . . . . . . . . . . . . . . 366.3 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 437 Case study: Automated theorem finding in graph theory 457.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 457.2 Perform the methodology . . . . . . . . . . . . . . . . . . . . . . . 457.3 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 518 Discussion 529 Conclusions 559.1 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 559.2 Future works . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55Publications 57Bibliography 59; 指導教員 : 程京德
• DOI: 10.24561/00010360; https://doi.org/10.24561/00010360
• Persistent ID (NDL): info:ndljp/pid/9921981; https://dl.ndl.go.jp/pid/9921981
• Collection: 障害者向け資料
• Collection (Materials For Handicapped People:1): テキストデータ
• Collection (particular): 国立国会図書館デジタルコレクション > デジタル化資料 > 博士論文; https://dl.ndl.go.jp/collections/A00014
• Acquisition Basis: 博士論文（自動収集）
• Date Accepted (W3CDTF): 2016-04-01T14:32:40+09:00
• Date Created (W3CDTF): 2015-12-16
• Format (IMT): application/pdf
• Access Restrictions: 国立国会図書館内限定公開
• Service for the Digitized Contents Transmission Service: 図書館・個人送信対象外
• Availability of remote photoduplication service: 可
• Periodical Title (URI): http://dx.doi.org/10.24561/00010360; http://id.nii.ac.jp/1586/00010360/
• Data Provider (Database): 国立国会図書館 : 国立国会図書館デジタルコレクション; https://dl.ndl.go.jp

Table of Contents

2023-09-05 再収集