WEKO3
アイテム
{"_buckets": {"deposit": "cf79e8e5-4670-4831-b4c5-32a27f252b97"}, "_deposit": {"created_by": 3, "id": "92", "owners": [3], "pid": {"revision_id": 0, "type": "depid", "value": "92"}, "status": "published"}, "_oai": {"id": "oai:metro-cit.repo.nii.ac.jp:00000092", "sets": ["18"]}, "author_link": ["658", "657", "998"], "item_1_biblio_info_14": {"attribute_name": "書誌情報", "attribute_value_mlt": [{"bibliographicIssueDates": {"bibliographicIssueDate": "2010-03", "bibliographicIssueDateType": "Issued"}, "bibliographicPageEnd": "90", "bibliographicPageStart": "79", "bibliographicVolumeNumber": "4", "bibliographic_titles": [{"bibliographic_title": "東京都立産業技術高等専門学校研究紀要"}, {"bibliographic_title": "Research reports of Tokyo Metropolitan College of Industrial Technology", "bibliographic_titleLang": "en"}]}]}, "item_1_creator_6": {"attribute_name": "著者名(日)", "attribute_type": "creator", "attribute_value_mlt": [{"creatorNames": [{"creatorName": "中西 , 泰雄"}, {"creatorName": "ナカニシ, ヤスオ", "creatorNameLang": "ja-Kana"}], "nameIdentifiers": [{"nameIdentifier": "657", "nameIdentifierScheme": "WEKO"}]}]}, "item_1_creator_7": {"attribute_name": "著者名よみ", "attribute_type": "creator", "attribute_value_mlt": [{"creatorNames": [{"creatorName": "ナカニシ, ヤスオ"}], "nameIdentifiers": [{"nameIdentifier": "998", "nameIdentifierScheme": "WEKO"}]}]}, "item_1_creator_8": {"attribute_name": "著者名(英)", "attribute_type": "creator", "attribute_value_mlt": [{"creatorNames": [{"creatorName": "Nakanishi , Yasuo", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "658", "nameIdentifierScheme": "WEKO"}]}]}, "item_1_description_1": {"attribute_name": "ページ属性", "attribute_value_mlt": [{"subitem_description": "P(論文)", "subitem_description_type": "Other"}]}, "item_1_description_12": {"attribute_name": "抄録(英)", "attribute_value_mlt": [{"subitem_description": "In a heuristic process of proof in mathematics, we try not only forward derivations from the assumptionssuch as `from A, we get B\u0027 but also backward derivations from the conclusion such as `in order to get A, we needB\u0027. As the result, the order of the propositions in accomplished proof is different from the order in which we getthose propositions in the heuristic process. For planning of proof, it is important to express what we want to provenow and what we have got so far at each step in the heuristic process. However, this expression is different fromthe proof itself by the above reason. In this paper, we suggest a method of planning proof by using `sequents\u0027 forthe expression of assumptions and conclusions. For a concrete study, we use the first order NK system of Gentzento explain our method. Our method gives an algorithm to prove arbitrary tautologies of the first order NK system,and is also valid for practical mathematics which is not necessarily formalized in symbolic logic.", "subitem_description_type": "Other"}]}, "item_1_source_id_13": {"attribute_name": "雑誌書誌ID", "attribute_value_mlt": [{"subitem_source_identifier": "AA12210629", "subitem_source_identifier_type": "NCID"}]}, "item_1_text_9": {"attribute_name": "著者所属(日)", "attribute_value_mlt": [{"subitem_text_value": "東京都立産業技術高等専門学校一般科"}]}, "item_files": {"attribute_name": "ファイル情報", "attribute_type": "file", "attribute_value_mlt": [{"accessrole": "open_date", "date": [{"dateType": "Available", "dateValue": "2010-03-01"}], "displaytype": "detail", "download_preview_message": "", "file_order": 0, "filename": "KJ00006858183.pdf", "filesize": [{"value": "94.5 kB"}], "format": "application/pdf", "future_date_message": "", "is_thumbnail": false, "licensetype": "license_11", "mimetype": "application/pdf", "size": 94500.0, "url": {"label": "KJ00006858183", "url": "https://metro-cit.repo.nii.ac.jp/record/92/files/KJ00006858183.pdf"}, "version_id": "431e1179-280c-4913-820b-e9d45c4f35c3"}]}, "item_keyword": {"attribute_name": "キーワード", "attribute_value_mlt": [{"subitem_subject": "Proof", "subitem_subject_language": "en", "subitem_subject_scheme": "Other"}, {"subitem_subject": "Sequent", "subitem_subject_language": "en", "subitem_subject_scheme": "Other"}, {"subitem_subject": "NK", "subitem_subject_language": "en", "subitem_subject_scheme": "Other"}]}, "item_language": {"attribute_name": "言語", "attribute_value_mlt": [{"subitem_language": "jpn"}]}, "item_resource_type": {"attribute_name": "資源タイプ", "attribute_value_mlt": [{"resourcetype": "departmental bulletin paper", "resourceuri": "http://purl.org/coar/resource_type/c_6501"}]}, "item_title": "シーケントを用いた証明計画法", "item_titles": {"attribute_name": "タイトル", "attribute_value_mlt": [{"subitem_title": "シーケントを用いた証明計画法"}, {"subitem_title": "Planning of Proof by means of Sequents", "subitem_title_language": "en"}]}, "item_type_id": "1", "owner": "3", "path": ["18"], "permalink_uri": "https://metro-cit.repo.nii.ac.jp/records/92", "pubdate": {"attribute_name": "公開日", "attribute_value": "2010-03-01"}, "publish_date": "2010-03-01", "publish_status": "0", "recid": "92", "relation": {}, "relation_version_is_last": true, "title": ["シーケントを用いた証明計画法"], "weko_shared_id": 3}
シーケントを用いた証明計画法
https://metro-cit.repo.nii.ac.jp/records/92
https://metro-cit.repo.nii.ac.jp/records/929cbdd9d3-cfb4-4091-83d2-ed8af092137e
名前 / ファイル | ライセンス | アクション |
---|---|---|
KJ00006858183 (94.5 kB)
|
Item type | 紀要論文(ELS) / Departmental Bulletin Paper(1) | |||||
---|---|---|---|---|---|---|
公開日 | 2010-03-01 | |||||
タイトル | ||||||
タイトル | シーケントを用いた証明計画法 | |||||
タイトル | ||||||
言語 | en | |||||
タイトル | Planning of Proof by means of Sequents | |||||
言語 | ||||||
言語 | jpn | |||||
キーワード | ||||||
言語 | en | |||||
主題 | Proof | |||||
キーワード | ||||||
言語 | en | |||||
主題 | Sequent | |||||
キーワード | ||||||
言語 | en | |||||
主題 | NK | |||||
資源タイプ | ||||||
資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||
資源タイプ | departmental bulletin paper | |||||
ページ属性 | ||||||
内容記述タイプ | Other | |||||
内容記述 | P(論文) | |||||
著者名(日) |
中西 , 泰雄
× 中西 , 泰雄 |
|||||
著者名よみ |
ナカニシ, ヤスオ
× ナカニシ, ヤスオ |
|||||
著者名(英) |
Nakanishi , Yasuo
× Nakanishi , Yasuo |
|||||
著者所属(日) | ||||||
東京都立産業技術高等専門学校一般科 | ||||||
抄録(英) | ||||||
内容記述タイプ | Other | |||||
内容記述 | In a heuristic process of proof in mathematics, we try not only forward derivations from the assumptionssuch as `from A, we get B' but also backward derivations from the conclusion such as `in order to get A, we needB'. As the result, the order of the propositions in accomplished proof is different from the order in which we getthose propositions in the heuristic process. For planning of proof, it is important to express what we want to provenow and what we have got so far at each step in the heuristic process. However, this expression is different fromthe proof itself by the above reason. In this paper, we suggest a method of planning proof by using `sequents' forthe expression of assumptions and conclusions. For a concrete study, we use the first order NK system of Gentzento explain our method. Our method gives an algorithm to prove arbitrary tautologies of the first order NK system,and is also valid for practical mathematics which is not necessarily formalized in symbolic logic. | |||||
雑誌書誌ID | ||||||
収録物識別子タイプ | NCID | |||||
収録物識別子 | AA12210629 | |||||
書誌情報 |
東京都立産業技術高等専門学校研究紀要 en : Research reports of Tokyo Metropolitan College of Industrial Technology 巻 4, p. 79-90, 発行日 2010-03 |