{"_buckets": {"deposit": "77ba1dc2-292b-4a3b-84e3-0e72ef3e840b"}, "_deposit": {"id": "19063", "owners": [], "pid": {"revision_id": 0, "type": "depid", "value": "19063"}, "status": "published"}, "_oai": {"id": "oai:nagoya.repo.nii.ac.jp:00019063"}, "item_10_alternative_title_19": {"attribute_name": "\u305d\u306e\u4ed6\u306e\u8a00\u8a9e\u306e\u30bf\u30a4\u30c8\u30eb", "attribute_value_mlt": [{"subitem_alternative_title": "Lemma Generation Method in Rewriting Induction for Constrained Term Rewriting Systems"}]}, "item_10_biblio_info_6": {"attribute_name": "\u66f8\u8a8c\u60c5\u5831", "attribute_value_mlt": [{"bibliographicIssueDates": {"bibliographicIssueDate": "2011-02", "bibliographicIssueDateType": "Issued"}, "bibliographicIssueNumber": "1", "bibliographicPageEnd": "189", "bibliographicPageStart": "173", "bibliographicVolumeNumber": "28", "bibliographic_titles": [{"bibliographic_title": "\u30b3\u30f3\u30d4\u30e5\u30fc\u30bf\u30bd\u30d5\u30c8\u30a6\u30a7\u30a2"}]}]}, "item_10_description_4": {"attribute_name": "\u6284\u9332", "attribute_value_mlt": [{"subitem_description": "\u8fd1\u5e74\uff0c\u5e30\u7d0d\u7684\u5b9a\u7406\u306e\u8a3c\u660e\u539f\u7406\u306e1\u3064\u3067\u3042\u308b\u66f8\u63db\u3048\u5e30\u7d0d\u6cd5\u304c\u5236\u7d04\u4ed8\u304d\u9805\u66f8\u63db\u3048\u7cfb\u306b\u5bfe\u5fdc\u3059\u308b\u3088\u3046\u306b\u62e1\u5f35\u3055\u308c\uff0c\u547d\u4ee4\u578b\u30d7\u30ed\u30b0\u30e9\u30e0\u306e\u7b49\u4fa1\u6027\u691c\u8a3c\u306b\u5fdc\u7528\u3059\u308b\u305f\u3081\u306e\u67a0\u7d44\u307f\u304c\u63d0\u6848\u3055\u308c\u305f\uff0e\u5e30\u7d0d\u7684\u5b9a\u7406\u306e\u8a3c\u660e\u306e\u305f\u3081\u306b\u306f\u9069\u5207\u306a\u88dc\u984c\u7b49\u5f0f\u3092\u4e0e\u3048\u308b\u5fc5\u8981\u304c\u3042\u308b\u5834\u5408\u304c\u591a\u3044\u304c\uff0c\u9805\u66f8\u63db\u3048\u7cfb\u306b\u304a\u3044\u3066\u3053\u308c\u307e\u3067\u7814\u7a76\u304c\u9032\u3093\u3067\u3044\u308b\u88dc\u984c\u751f\u6210\u306e\u624b\u6cd5\u3092\u5236\u7d04\u4ed8\u304d\u9805\u66f8\u63db\u3048\u7cfb\u306b\u5bfe\u3057\u3066\u5229\u7528\u3059\u308b\u305f\u3081\u306b\u306f\u5236\u7d04\u90e8\u5206\u3092\u6271\u3046\u305f\u3081\u306e\u62e1\u5f35\u304c\u5fc5\u8981\u3067\u3042\u308b\uff0e\u672c\u8ad6\u6587\u3067\u306f\uff0c\u66f8\u63db\u3048\u898f\u5247\u304b\u3089\u9805\u306e\u95a2\u4fc2\u3092\u5b9a\u5f0f\u5316\u3057\uff0c\u305d\u306e\u95a2\u4fc2\u306b\u57fa\u3065\u3044\u3066\u7b49\u5f0f\u3092\u3088\u308a\u4e00\u822c\u7684\u306a\u7b49\u5f0f\u306b\u5909\u63db\u3059\u308b\u67a0\u7d44\u307f\u3092\u63d0\u6848\u3059\u308b\uff0e\u3055\u3089\u306b\uff0c\u5236\u7d04\u4ed8\u304d\u9805\u66f8\u63db\u3048\u7cfb\u306e\u66f8\u63db\u3048\u5e30\u7d0d\u6cd5\u306b\u3088\u308b\u8a3c\u660e\u624b\u7d9a\u304d\u306b\u305d\u306e\u67a0\u7d44\u307f\u3092\u5229\u7528\u3057\u305f\u88dc\u984c\u7b49\u5f0f\u306e\u751f\u6210\u30fb\u8ffd\u52a0\u6a5f\u80fd\u3092\u7d44\u307f\u8fbc\u3080\u3053\u3068\u3067\uff0c\u88dc\u984c\u7b49\u5f0f\u3092\u4e88\u3081\u8a18\u8ff0\u305b\u305a\u306b\u5b9a\u7406\u81ea\u52d5\u8a3c\u660e\u3092\u8a66\u307f\uff0c\u305d\u306e\u6709\u52b9\u6027\u3092\u691c\u8a3c\u3059\u308b\uff0eRecently, the rewriting induction, which is one of induction principles for proving inductive theorems of an equational theory, has been extended to deal with constrained term rewriting systems. It has been applied to developing a method for proving equivalence of imperative programs. For proving inductive theorem, there are many cases where appropriate lemmas need to be added. To this end, several methods for lemma generation in term rewriting have been studied. However, these existing methods are not effective for cases in constrained term rewriting. In this paper, we propose a framework of lemma generation for constrained term rewriting systems, in which we formalize the correspondences of terms in divergent equations by means of given constrained rewrite rules. We also show an instance of the formalization, and show that due to the framework with the instance, there is no necessity to give lemmas in advance in the examples shown by the previous works.", "subitem_description_type": "Abstract"}]}, "item_10_identifier_60": {"attribute_name": "URI", "attribute_value_mlt": [{"subitem_identifier_type": "DOI", "subitem_identifier_uri": "http://dx.doi.org/10.11309/jssst.28.1_173"}, {"subitem_identifier_type": "HDL", "subitem_identifier_uri": "http://hdl.handle.net/2237/21169"}]}, "item_10_publisher_32": {"attribute_name": "\u51fa\u7248\u8005", "attribute_value_mlt": [{"subitem_publisher": "\u65e5\u672c\u30bd\u30d5\u30c8\u30a6\u30a7\u30a2\u79d1\u5b66\u4f1a"}]}, "item_10_rights_12": {"attribute_name": "\u6a29\u5229", "attribute_value_mlt": [{"subitem_rights": "\u3053\u3053\u306b\u63b2\u8f09\u3057\u305f\u8457\u4f5c\u7269\u306e\u5229\u7528\u306b\u95a2\u3059\u308b\u6ce8\u610f \u672c\u8457\u4f5c\u7269\u306e\u8457\u4f5c\u6a29\u306f\u65e5\u672c\u30bd\u30d5\u30c8\u30a6\u30a7\u30a2\u79d1\u5b66\u4f1a\u306b\u5e30\u5c5e\u3057\u307e\u3059\uff0e\u672c\u8457\u4f5c\u7269\u306f\u8457\u4f5c\u6a29\u8005\u3067\u3042\u308b\u65e5\u672c\u30bd\u30d5\u30c8\u30a6\u30a7\u30a2\u79d1\u5b66\u4f1a\u306e\u8a31\u53ef\u306e\u3082\u3068\u306b\u63b2\u8f09\u3059\u308b\u3082\u306e\u3067\u3059\uff0e\u3054\u5229\u7528\u306b\u5f53\u305f\u3063\u3066\u306f\u300c\u8457\u4f5c\u6a29\u6cd5\u300d\u306b\u5f93\u3046\u3053\u3068\u3092\u304a\u9858\u3044\u3044\u305f\u3057\u307e\u3059\uff0eNotice for the use of this material: The copyright of this material is retained by the Japan Society for Software Science and Technology (JSSST). This material is published on this web site with the agreement of the JSSST. Please be complied with Copyright Law of Japan if any users wish to reproduce, make derivative work, distribute or make available to the public any part or whole thereof."}, {"subitem_rights": "\u672c\u6587\u30c7\u30fc\u30bf\u306f\u5b66\u4f1a\u306e\u8a31\u8afe\u306b\u57fa\u3065\u304dJ-STAGE\u3088\u308a\u8907\u88fd\u3057\u305f\u3082\u306e\u3067\u3042\u308b\u3002"}]}, "item_10_select_15": {"attribute_name": "\u8457\u8005\u7248\u30d5\u30e9\u30b0", "attribute_value_mlt": [{"subitem_select_item": "publisher"}]}, "item_10_source_id_7": {"attribute_name": "ISSN", "attribute_value_mlt": [{"subitem_source_identifier": "0289-6540", "subitem_source_identifier_type": "ISSN"}]}, "item_creator": {"attribute_name": "\u8457\u8005", "attribute_type": "creator", "attribute_value_mlt": [{"creatorNames": [{"creatorName": "\u4e2d\u6797, \u76f4\u751f"}], "nameIdentifiers": [{"nameIdentifier": "55697", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "\u897f\u7530, \u76f4\u6a39"}], "nameIdentifiers": [{"nameIdentifier": "55698", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "\u8349\u5208, \u572d\u4e00\u6717"}], "nameIdentifiers": [{"nameIdentifier": "55699", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "\u5742\u90e8, \u4fca\u6a39"}], "nameIdentifiers": [{"nameIdentifier": "55700", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "\u9152\u4e95, \u6b63\u5f66"}], "nameIdentifiers": [{"nameIdentifier": "55701", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "Nakabayashi, Naoki"}], "nameIdentifiers": [{"nameIdentifier": "55702", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "Nishida, Naoki"}], "nameIdentifiers": [{"nameIdentifier": "55703", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "Kusakari, Keiichirou"}], "nameIdentifiers": [{"nameIdentifier": "55704", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "Sakabe, Toshiki"}], "nameIdentifiers": [{"nameIdentifier": "55705", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "Sakai, Masahiko"}], "nameIdentifiers": [{"nameIdentifier": "55706", "nameIdentifierScheme": "WEKO"}]}]}, "item_files": {"attribute_name": "\u30d5\u30a1\u30a4\u30eb\u60c5\u5831", "attribute_type": "file", "attribute_value_mlt": [{"accessrole": "open_date", "date": [{"dateType": "Available", "dateValue": "2018-02-21"}], "displaytype": "detail", "download_preview_message": "", "file_order": 0, "filename": "28_1_173.pdf", "filesize": [{"value": "241.0 kB"}], "format": "application/pdf", "future_date_message": "", "is_thumbnail": false, "licensetype": "license_free", "mimetype": "application/pdf", "size": 241000.0, "url": {"label": "28_1_173.pdf", "url": "https://nagoya.repo.nii.ac.jp/record/19063/files/28_1_173.pdf"}, "version_id": "c2ba2085-066f-44cc-adff-5702e837c1a2"}]}, "item_language": {"attribute_name": "\u8a00\u8a9e", "attribute_value_mlt": [{"subitem_language": "jpn"}]}, "item_resource_type": {"attribute_name": "\u8cc7\u6e90\u30bf\u30a4\u30d7", "attribute_value_mlt": [{"resourcetype": "journal article", "resourceuri": "http://purl.org/coar/resource_type/c_6501"}]}, "item_title": "\u5236\u7d04\u4ed8\u304d\u9805\u66f8\u63db\u3048\u7cfb\u306e\u66f8\u63db\u3048\u5e30\u7d0d\u6cd5\u306b\u304a\u3051\u308b\u88dc\u984c\u7b49\u5f0f\u306e\u81ea\u52d5\u751f\u6210\u6cd5", "item_titles": {"attribute_name": "\u30bf\u30a4\u30c8\u30eb", "attribute_value_mlt": [{"subitem_title": "\u5236\u7d04\u4ed8\u304d\u9805\u66f8\u63db\u3048\u7cfb\u306e\u66f8\u63db\u3048\u5e30\u7d0d\u6cd5\u306b\u304a\u3051\u308b\u88dc\u984c\u7b49\u5f0f\u306e\u81ea\u52d5\u751f\u6210\u6cd5"}]}, "item_type_id": "10", "owner": "1", "path": ["312/313/314"], "permalink_uri": "http://hdl.handle.net/2237/21169", "pubdate": {"attribute_name": "\u516c\u958b\u65e5", "attribute_value": "2015-01-30"}, "publish_date": "2015-01-30", "publish_status": "0", "recid": "19063", "relation": {}, "relation_version_is_last": true, "title": ["\u5236\u7d04\u4ed8\u304d\u9805\u66f8\u63db\u3048\u7cfb\u306e\u66f8\u63db\u3048\u5e30\u7d0d\u6cd5\u306b\u304a\u3051\u308b\u88dc\u984c\u7b49\u5f0f\u306e\u81ea\u52d5\u751f\u6210\u6cd5"], "weko_shared_id": null}