{"_buckets": {"deposit": "cea9350b-e7a9-497f-9586-faa82efdf35f"}, "_deposit": {"created_by": 3, "id": "145", "owners": [3], "pid": {"revision_id": 0, "type": "depid", "value": "145"}, "status": "published"}, "_oai": {"id": "oai:metro-cit.repo.nii.ac.jp:00000145", "sets": ["21"]}, "author_link": ["658", "657", "998"], "item_1_biblio_info_14": {"attribute_name": "書誌情報", "attribute_value_mlt": [{"bibliographicIssueDates": {"bibliographicIssueDate": "2013-03", "bibliographicIssueDateType": "Issued"}, "bibliographicPageEnd": "40", "bibliographicPageStart": "26", "bibliographicVolumeNumber": "7", "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 derivationsfrom the assumptions such as `from A, we get B\u0027 but also backward derivations from theconclusion such as `in order to get C, we need D\u0027. Thus, we have to discover all the statementswhich connect assumptions with the conclusion, to complete the planning of the proof. Wedefine `heuristic tableau\u0027 as a tableau which consists of those statements aranged in the order of discovery with symbols which express the logical relations of those statements. We suggesta planning method of proofs by using heuristic tableaus. For a concrete explanation, we use the first order NK system of Gentzen to explain our method. Our method gives an algorithmto 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": "2013-03-01"}], "displaytype": "detail", "download_preview_message": "", "file_order": 0, "filename": "KJ00008928039.pdf", "filesize": [{"value": "95.7 kB"}], "format": "application/pdf", "future_date_message": "", "is_thumbnail": false, "licensetype": "license_11", "mimetype": "application/pdf", "size": 95700.0, "url": {"label": "KJ00008928039", "url": "https://metro-cit.repo.nii.ac.jp/record/145/files/KJ00008928039.pdf"}, "version_id": "d998d6e5-7f29-4bc7-a6cd-1a2a30375408"}]}, "item_keyword": {"attribute_name": "キーワード", "attribute_value_mlt": [{"subitem_subject": "Proo", "subitem_subject_language": "en", "subitem_subject_scheme": "Other"}, {"subitem_subject": "Heuristic Tableau", "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 Heuristic Tableau", "subitem_title_language": "en"}]}, "item_type_id": "1", "owner": "3", "path": ["21"], "permalink_uri": "https://metro-cit.repo.nii.ac.jp/records/145", "pubdate": {"attribute_name": "公開日", "attribute_value": "2013-03-01"}, "publish_date": "2013-03-01", "publish_status": "0", "recid": "145", "relation": {}, "relation_version_is_last": true, "title": ["発見タブローによる証明計画"], "weko_shared_id": 3}