WEKO3
アイテム
{"_buckets": {"deposit": "11c2473b-12e1-424e-b02c-70215bf8afcb"}, "_deposit": {"created_by": 15, "id": "10366", "owners": [15], "pid": {"revision_id": 0, "type": "depid", "value": "10366"}, "status": "published"}, "_oai": {"id": "oai:sucra.repo.nii.ac.jp:00010366", "sets": ["506"]}, "author_link": [], "item_113_alternative_title_1": {"attribute_name": "タイトル(別言語)", "attribute_value_mlt": [{"subitem_alternative_title": "強相関論理に基づく前向き推論による自動定理発見 : 方法論と事例研究"}]}, "item_113_biblio_info_9": {"attribute_name": "書誌情報", "attribute_value_mlt": [{"bibliographicIssueDates": {"bibliographicIssueDate": "2015", "bibliographicIssueDateType": "Issued"}}]}, "item_113_date_35": {"attribute_name": "作成日", "attribute_value_mlt": [{"subitem_date_issued_datetime": "2015-12-16", "subitem_date_issued_type": "Created"}]}, "item_113_date_granted_20": {"attribute_name": "学位授与年月日", "attribute_value_mlt": [{"subitem_dategranted": "2015-03-24"}]}, "item_113_degree_grantor_22": {"attribute_name": "学位授与機関", "attribute_value_mlt": [{"subitem_degreegrantor": [{"subitem_degreegrantor_name": "埼玉大学"}], "subitem_degreegrantor_identifier": [{"subitem_degreegrantor_identifier_name": "12401", "subitem_degreegrantor_identifier_scheme": "kakenhi"}]}]}, "item_113_degree_name_21": {"attribute_name": "学位名", "attribute_value_mlt": [{"subitem_degreename": "博士(工学)"}]}, "item_113_description_13": {"attribute_name": "形態", "attribute_value_mlt": [{"subitem_description": "vii, 62 p.", "subitem_description_type": "Other"}]}, "item_113_description_23": {"attribute_name": "抄録", "attribute_value_mlt": [{"subitem_description": "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.\nThe 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\u0027s 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.\nCheng 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.\nThis 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.\nIn 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\u0027s 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.\nThis 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.\nThis 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\u0027s 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.", "subitem_description_type": "Abstract"}]}, "item_113_description_24": {"attribute_name": "目次", "attribute_value_mlt": [{"subitem_description": "Abstract i\nAcknowledgments iii\nList of figures vi\nList of tables vii\n1 Introduction 1\n1.1 Background and motivation . . . . . . . . . . . . . . . . . . . . . . 1\n1.2 Purpose and objectives . . . . . . . . . . . . . . . . . . . . . . . . . 3\n1.3 Structure of the thesis . . . . . . . . . . . . . . . . . . . . . . . . . 3\n2 Basic notions and notations 5\n2.1 Logic-based reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . 5\n2.2 Strong relevant logics . . . . . . . . . . . . . . . . . . . . . . . . . . 6\n2.3 Forward deduction engine . . . . . . . . . . . . . . . . . . . . . . . 10\n2.4 The semi-lattice model of formal theories . . . . . . . . . . . . . . . 11\n3 A systematic methodology for automated theorem finding 13\n3.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13\n3.2 Systematic methodology . . . . . . . . . . . . . . . . . . . . . . . . 13\n4 Preparation of logical fragments 21\n5 Case study: Automated theorem finding in NBG set theory 24\n5.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24\n5.2 Perform the methodology . . . . . . . . . . . . . . . . . . . . . . . 24\n5.3 Case study for explicitly epistemic contraction by predicate abstracton 31\n5.4 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34\n6 Case study: Automated theorem finding in Peano\u0027s arithmetic 36\n6.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36\n6.2 Perform the methodology . . . . . . . . . . . . . . . . . . . . . . . 36\n6.3 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43\n7 Case study: Automated theorem finding in graph theory 45\n7.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45\n7.2 Perform the methodology . . . . . . . . . . . . . . . . . . . . . . . 45\n7.3 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51\n8 Discussion 52\n9 Conclusions 55\n9.1 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55\n9.2 Future works . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55\nPublications 57\nBibliography 59", "subitem_description_type": "Other"}]}, "item_113_description_25": {"attribute_name": "注記", "attribute_value_mlt": [{"subitem_description": "指導教員 : 程京德", "subitem_description_type": "Other"}]}, "item_113_description_33": {"attribute_name": "資源タイプ", "attribute_value_mlt": [{"subitem_description": "text", "subitem_description_type": "Other"}]}, "item_113_description_34": {"attribute_name": "フォーマット", "attribute_value_mlt": [{"subitem_description": "application/pdf", "subitem_description_type": "Other"}]}, "item_113_dissertation_number_19": {"attribute_name": "学位授与番号", "attribute_value_mlt": [{"subitem_dissertationnumber": "甲第984号"}]}, "item_113_identifier_registration": {"attribute_name": "ID登録", "attribute_value_mlt": [{"subitem_identifier_reg_text": "10.24561/00010360", "subitem_identifier_reg_type": "JaLC"}]}, "item_113_publisher_11": {"attribute_name": "出版者名", "attribute_value_mlt": [{"subitem_publisher": "埼玉大学大学院理工学研究科"}]}, "item_113_publisher_12": {"attribute_name": "出版者名(別言語)", "attribute_value_mlt": [{"subitem_publisher": "Graduate School of Science and Engineering, Saitama University"}]}, "item_113_record_name_8": {"attribute_name": "書誌", "attribute_value_mlt": [{"subitem_record_name": "博士論文(埼玉大学大学院理工学研究科(博士後期課程))"}]}, "item_113_text_3": {"attribute_name": "著者 ローマ字", "attribute_value_mlt": [{"subitem_text_value": "GAO, Hongbiao"}]}, "item_113_text_31": {"attribute_name": "版", "attribute_value_mlt": [{"subitem_text_value": "[出版社版]"}]}, "item_113_text_36": {"attribute_name": "アイテムID", "attribute_value_mlt": [{"subitem_text_value": "GD0000647"}]}, "item_113_text_4": {"attribute_name": "著者 所属", "attribute_value_mlt": [{"subitem_text_value": "埼玉大学大学院理工学研究科(博士後期課程)理工学専攻"}]}, "item_113_text_5": {"attribute_name": "著者 所属(別言語)", "attribute_value_mlt": [{"subitem_text_value": "Graduate School of Science and Engineering, Saitama University"}]}, "item_113_version_type_32": {"attribute_name": "著者版フラグ", "attribute_value_mlt": [{"subitem_version_resource": "http://purl.org/coar/version/c_970fb48d4fbd8a85", "subitem_version_type": "VoR"}]}, "item_access_right": {"attribute_name": "アクセス権", "attribute_value_mlt": [{"subitem_access_right": "open access", "subitem_access_right_uri": "http://purl.org/coar/access_right/c_abf2"}]}, "item_creator": {"attribute_name": "著者", "attribute_type": "creator", "attribute_value_mlt": [{"creatorNames": [{"creatorName": "高, 宏彪", "creatorNameLang": "ja"}, {"creatorName": "コウ, コウヒョウ", "creatorNameLang": "ja-Kana"}]}]}, "item_files": {"attribute_name": "ファイル情報", "attribute_type": "file", "attribute_value_mlt": [{"accessrole": "open_date", "date": [{"dateType": "Available", "dateValue": "2018-01-23"}], "displaytype": "detail", "download_preview_message": "", "file_order": 0, "filename": "GD0000647.pdf", "filesize": [{"value": "2.7 MB"}], "format": "application/pdf", "future_date_message": "", "is_thumbnail": false, "licensetype": "license_note", "mimetype": "application/pdf", "size": 2700000.0, "url": {"label": "GD0000647.pdf", "objectType": "fulltext", "url": "https://sucra.repo.nii.ac.jp/record/10366/files/GD0000647.pdf"}, "version_id": "86e6e1ae-e339-43bd-af71-85619a7738d4"}]}, "item_language": {"attribute_name": "言語", "attribute_value_mlt": [{"subitem_language": "eng"}]}, "item_resource_type": {"attribute_name": "資源タイプ", "attribute_value_mlt": [{"resourcetype": "doctoral thesis", "resourceuri": "http://purl.org/coar/resource_type/c_db06"}]}, "item_title": "Automated Theorem Finding by Forward Reasoning Based on Strong Relevant Logic : Methodology and Case Studies", "item_titles": {"attribute_name": "タイトル", "attribute_value_mlt": [{"subitem_title": "Automated Theorem Finding by Forward Reasoning Based on Strong Relevant Logic : Methodology and Case Studies", "subitem_title_language": "en"}]}, "item_type_id": "113", "owner": "15", "path": ["506"], "permalink_uri": "https://doi.org/10.24561/00010360", "pubdate": {"attribute_name": "PubDate", "attribute_value": "2015-12-17"}, "publish_date": "2015-12-17", "publish_status": "0", "recid": "10366", "relation": {}, "relation_version_is_last": true, "title": ["Automated Theorem Finding by Forward Reasoning Based on Strong Relevant Logic : Methodology and Case Studies"], "weko_shared_id": -1}
Automated Theorem Finding by Forward Reasoning Based on Strong Relevant Logic : Methodology and Case Studies
https://doi.org/10.24561/00010360
https://doi.org/10.24561/000103603da8289e-7097-497d-8409-c8c5ff285373
名前 / ファイル | ライセンス | アクション |
---|---|---|
GD0000647.pdf (2.7 MB)
|
|
Item type | 学位論文 / Thesis or Dissertation(1) | |||||||||
---|---|---|---|---|---|---|---|---|---|---|
公開日 | 2015-12-17 | |||||||||
タイトル | ||||||||||
言語 | en | |||||||||
タイトル | Automated Theorem Finding by Forward Reasoning Based on Strong Relevant Logic : Methodology and Case Studies | |||||||||
言語 | ||||||||||
言語 | eng | |||||||||
資源タイプ | ||||||||||
資源タイプ識別子 | http://purl.org/coar/resource_type/c_db06 | |||||||||
資源タイプ | doctoral thesis | |||||||||
ID登録 | ||||||||||
ID登録 | 10.24561/00010360 | |||||||||
ID登録タイプ | JaLC | |||||||||
アクセス権 | ||||||||||
アクセス権 | open access | |||||||||
アクセス権URI | http://purl.org/coar/access_right/c_abf2 | |||||||||
タイトル(別言語) | ||||||||||
その他のタイトル | 強相関論理に基づく前向き推論による自動定理発見 : 方法論と事例研究 | |||||||||
著者 |
高, 宏彪
× 高, 宏彪
|
|||||||||
著者 ローマ字 | ||||||||||
GAO, Hongbiao | ||||||||||
著者 所属 | ||||||||||
埼玉大学大学院理工学研究科(博士後期課程)理工学専攻 | ||||||||||
著者 所属(別言語) | ||||||||||
Graduate School of Science and Engineering, Saitama University | ||||||||||
書誌 | ||||||||||
収録物名 | 博士論文(埼玉大学大学院理工学研究科(博士後期課程)) | |||||||||
書誌情報 |
発行日 2015 |
|||||||||
出版者名 | ||||||||||
出版者 | 埼玉大学大学院理工学研究科 | |||||||||
出版者名(別言語) | ||||||||||
出版者 | Graduate School of Science and Engineering, Saitama University | |||||||||
形態 | ||||||||||
内容記述タイプ | Other | |||||||||
内容記述 | vii, 62 p. | |||||||||
学位授与番号 | ||||||||||
学位授与番号 | 甲第984号 | |||||||||
学位授与年月日 | ||||||||||
学位授与年月日 | 2015-03-24 | |||||||||
学位名 | ||||||||||
学位名 | 博士(工学) | |||||||||
学位授与機関 | ||||||||||
学位授与機関識別子Scheme | kakenhi | |||||||||
学位授与機関識別子 | 12401 | |||||||||
学位授与機関名 | 埼玉大学 | |||||||||
抄録 | ||||||||||
内容記述タイプ | 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. 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. |
|||||||||
目次 | ||||||||||
内容記述タイプ | Other | |||||||||
内容記述 | Abstract i Acknowledgments iii List of figures vi List of tables vii 1 Introduction 1 1.1 Background and motivation . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Purpose and objectives . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.3 Structure of the thesis . . . . . . . . . . . . . . . . . . . . . . . . . 3 2 Basic notions and notations 5 2.1 Logic-based reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.2 Strong relevant logics . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.3 Forward deduction engine . . . . . . . . . . . . . . . . . . . . . . . 10 2.4 The semi-lattice model of formal theories . . . . . . . . . . . . . . . 11 3 A systematic methodology for automated theorem finding 13 3.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 3.2 Systematic methodology . . . . . . . . . . . . . . . . . . . . . . . . 13 4 Preparation of logical fragments 21 5 Case study: Automated theorem finding in NBG set theory 24 5.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 5.2 Perform the methodology . . . . . . . . . . . . . . . . . . . . . . . 24 5.3 Case study for explicitly epistemic contraction by predicate abstracton 31 5.4 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 6 Case study: Automated theorem finding in Peano's arithmetic 36 6.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 6.2 Perform the methodology . . . . . . . . . . . . . . . . . . . . . . . 36 6.3 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 7 Case study: Automated theorem finding in graph theory 45 7.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 7.2 Perform the methodology . . . . . . . . . . . . . . . . . . . . . . . 45 7.3 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 8 Discussion 52 9 Conclusions 55 9.1 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 9.2 Future works . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 Publications 57 Bibliography 59 |
|||||||||
注記 | ||||||||||
内容記述タイプ | Other | |||||||||
内容記述 | 指導教員 : 程京德 | |||||||||
版 | ||||||||||
[出版社版] | ||||||||||
著者版フラグ | ||||||||||
出版タイプ | VoR | |||||||||
出版タイプResource | http://purl.org/coar/version/c_970fb48d4fbd8a85 | |||||||||
資源タイプ | ||||||||||
内容記述タイプ | Other | |||||||||
内容記述 | text | |||||||||
フォーマット | ||||||||||
内容記述タイプ | Other | |||||||||
内容記述 | application/pdf | |||||||||
作成日 | ||||||||||
日付 | 2015-12-16 | |||||||||
日付タイプ | Created | |||||||||
アイテムID | ||||||||||
GD0000647 |