{"_buckets": {"deposit": "f96885ff-152f-476c-92aa-2115b2c2fb59"}, "_deposit": {"id": "7860", "owners": [], "pid": {"revision_id": 0, "type": "depid", "value": "7860"}, "status": "published"}, "_oai": {"id": "oai:nagoya.repo.nii.ac.jp:00007860", "sets": ["314"]}, "author_link": ["22465", "22466", "22467"], "item_10_biblio_info_6": {"attribute_name": "書誌情報", "attribute_value_mlt": [{"bibliographicIssueDates": {"bibliographicIssueDate": "2005-12", "bibliographicIssueDateType": "Issued"}, "bibliographicIssueNumber": "12", "bibliographicPageEnd": "2726", "bibliographicPageStart": "2715", "bibliographicVolumeNumber": "E88-D", "bibliographic_titles": [{"bibliographic_title": "IEICE Transactions on Information and Systems", "bibliographic_titleLang": "en"}]}]}, "item_10_description_4": {"attribute_name": "抄録", "attribute_value_mlt": [{"subitem_description": "Automated reasoning of inductive theorems is considered important in program verification. To verify inductive theorems automatically, several implicit induction methods like the inductionless induction and the rewriting induction methods have been proposed. In studying inductive theorems on higher-order rewritings, we found that the class of the theorems shown by known implicit induction methods does not coincide with that of inductive theorems, and the gap between them is a barrier in developing mechanized methods for disproving inductive theorems. This paper fills this gap by introducing the notion of primitive inductive theorems, and clarifying the relation between inductive theorems and primitive inductive theorems. Based on this relation, we achieve mechanized methods for proving and disproving inductive theorems.", "subitem_description_language": "en", "subitem_description_type": "Abstract"}]}, "item_10_identifier_60": {"attribute_name": "URI", "attribute_value_mlt": [{"subitem_identifier_type": "HDL", "subitem_identifier_uri": "http://hdl.handle.net/2237/9580"}]}, "item_10_publisher_32": {"attribute_name": "出版者", "attribute_value_mlt": [{"subitem_publisher": "IEICE", "subitem_publisher_language": "ja"}]}, "item_10_rights_12": {"attribute_name": "権利", "attribute_value_mlt": [{"subitem_rights": "Copyright 2005 IEICE 許諾番号 08RB0027号", "subitem_rights_language": "ja"}]}, "item_10_select_15": {"attribute_name": "著者版フラグ", "attribute_value_mlt": [{"subitem_select_item": "publisher"}]}, "item_10_source_id_7": {"attribute_name": "ISSN", "attribute_value_mlt": [{"subitem_source_identifier": "0916-8532", "subitem_source_identifier_type": "PISSN"}]}, "item_10_text_14": {"attribute_name": "フォーマット", "attribute_value_mlt": [{"subitem_text_value": "application/pdf"}]}, "item_1615787544753": {"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": "KUSAKARI, Keiichirou", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "22465", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "SAKAI, Masahiko", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "22466", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "SAKABE, Toshiki", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "22467", "nameIdentifierScheme": "WEKO"}]}]}, "item_files": {"attribute_name": "ファイル情報", "attribute_type": "file", "attribute_value_mlt": [{"accessrole": "open_date", "date": [{"dateType": "Available", "dateValue": "2018-02-19"}], "displaytype": "detail", "download_preview_message": "", "file_order": 0, "filename": "E88-D_n12_2715-2726.pdf", "filesize": [{"value": "1.3 MB"}], "format": "application/pdf", "future_date_message": "", "is_thumbnail": false, "licensetype": "license_note", "mimetype": "application/pdf", "size": 1300000.0, "url": {"label": "E88-D_n12_2715-2726.pdf", "objectType": "fulltext", "url": "https://nagoya.repo.nii.ac.jp/record/7860/files/E88-D_n12_2715-2726.pdf"}, "version_id": "f68428ed-9fd8-4d95-9c47-e54786958679"}]}, "item_keyword": {"attribute_name": "キーワード", "attribute_value_mlt": [{"subitem_subject": "algebraic specification", "subitem_subject_scheme": "Other"}, {"subitem_subject": "simply-typed term rewriting system", "subitem_subject_scheme": "Other"}, {"subitem_subject": "primitive inductive theorem", "subitem_subject_scheme": "Other"}, {"subitem_subject": "inductive theorem", "subitem_subject_scheme": "Other"}, {"subitem_subject": "implicit induction method", "subitem_subject_scheme": "Other"}]}, "item_language": {"attribute_name": "言語", "attribute_value_mlt": [{"subitem_language": "eng"}]}, "item_resource_type": {"attribute_name": "資源タイプ", "attribute_value_mlt": [{"resourcetype": "journal article", "resourceuri": "http://purl.org/coar/resource_type/c_6501"}]}, "item_title": "Primitive Inductive Theorems Bridge Implicit Induction Methods and Inductive Theorems in Higher-Order Rewriting", "item_titles": {"attribute_name": "タイトル", "attribute_value_mlt": [{"subitem_title": "Primitive Inductive Theorems Bridge Implicit Induction Methods and Inductive Theorems in Higher-Order Rewriting", "subitem_title_language": "en"}]}, "item_type_id": "10", "owner": "1", "path": ["314"], "permalink_uri": "http://hdl.handle.net/2237/9580", "pubdate": {"attribute_name": "PubDate", "attribute_value": "2008-03-10"}, "publish_date": "2008-03-10", "publish_status": "0", "recid": "7860", "relation": {}, "relation_version_is_last": true, "title": ["Primitive Inductive Theorems Bridge Implicit Induction Methods and Inductive Theorems in Higher-Order Rewriting"], "weko_shared_id": -1}