{"_buckets": {"deposit": "0de1467b-d009-4329-a539-3f280c48a4af"}, "_deposit": {"created_by": 17, "id": "2003931", "owner": "17", "owners": [17], "owners_ext": {"displayname": "repository", "username": "repository"}, "pid": {"revision_id": 0, "type": "depid", "value": "2003931"}, "status": "published"}, "_oai": {"id": "oai:nagoya.repo.nii.ac.jp:02003931", "sets": ["314"]}, "author_link": [], "item_1615768549627": {"attribute_name": "出版タイプ", "attribute_value_mlt": [{"subitem_version_resource": "http://purl.org/coar/version/c_ab4af688f83e57aa", "subitem_version_type": "AM"}]}, "item_1629683748249": {"attribute_name": "日付", "attribute_value_mlt": [{"subitem_date_issued_datetime": "2024-06-01", "subitem_date_issued_type": "Available"}]}, "item_9_biblio_info_6": {"attribute_name": "書誌情報", "attribute_value_mlt": [{"bibliographicIssueDates": {"bibliographicIssueDate": "2022-06", "bibliographicIssueDateType": "Issued"}, "bibliographicPageStart": "100779", "bibliographicVolumeNumber": "127", "bibliographic_titles": [{"bibliographic_title": "Journal of Logical and Algebraic Methods in Programming", "bibliographic_titleLang": "en"}]}]}, "item_9_description_4": {"attribute_name": "内容記述", "attribute_value_mlt": [{"subitem_description": "In this paper, we transform an orthogonal inductive definition set, which is a set of productions for inductive predicates, into a confluent term rewrite system such that a quantifier-free sequent is valid w.r.t. the inductive definition set if and only if an equation representing the sequent is an inductive theorem of the term rewrite system. To this end, we first propose a transformation of an orthogonal inductive definition set into a confluent term rewrite system that is equivalent to the inductive definition set in the sense of evaluating ground formulas. Then, we show that termination of the inductive definition set is proved by the generalized subterm criterion if and only if termination of the transformed term rewrite system is so. Finally, we show that the transformed term rewrite system with some rewrite rules for sequents has the expected property. In addition, we show a termination criterion for the union of term rewrite systems whose termination is proved by the generalized subterm criterion.", "subitem_description_language": "en", "subitem_description_type": "Abstract"}]}, "item_9_publisher_32": {"attribute_name": "出版者", "attribute_value_mlt": [{"subitem_publisher": "Elsevier", "subitem_publisher_language": "en"}]}, "item_9_relation_43": {"attribute_name": "関連情報", "attribute_value_mlt": [{"subitem_relation_type": "isVersionOf", "subitem_relation_type_id": {"subitem_relation_type_id_text": "https://doi.org/10.1016/j.jlamp.2022.100779", "subitem_relation_type_select": "DOI"}}]}, "item_9_rights_12": {"attribute_name": "権利", "attribute_value_mlt": [{"subitem_rights": "© 2022. This manuscript version is made available under the CC-BY-NC-ND 4.0 license http://creativecommons.org/licenses/by-nc-nd/4.0/", "subitem_rights_language": "en"}]}, "item_9_source_id_7": {"attribute_name": "収録物識別子", "attribute_value_mlt": [{"subitem_source_identifier": "2352-2208", "subitem_source_identifier_type": "PISSN"}]}, "item_access_right": {"attribute_name": "アクセス権", "attribute_value_mlt": [{"subitem_access_right": "embargoed access", "subitem_access_right_uri": "http://purl.org/coar/access_right/c_f1cf"}]}, "item_creator": {"attribute_name": "著者", "attribute_type": "creator", "attribute_value_mlt": [{"creatorNames": [{"creatorName": "Zhang, Shujun", "creatorNameLang": "en"}]}, {"creatorNames": [{"creatorName": "Nishida, Naoki", "creatorNameLang": "en"}]}]}, "item_files": {"attribute_name": "ファイル情報", "attribute_type": "file", "attribute_value_mlt": [{"accessrole": "open_date", "date": [{"dateType": "Available", "dateValue": "2024-06-01"}], "displaytype": "detail", "download_preview_message": "Download / Preview is available from 2024/5/31.", "file_order": 0, "filename": "ZhangNishida2022jlamp_preprint.pdf", "filesize": [{"value": "738 KB"}], "format": "application/pdf", "future_date_message": "Download is available from 2024/5/31.", "is_thumbnail": false, "mimetype": "application/pdf", "size": 738000.0, "url": {"objectType": "fulltext", "url": "https://nagoya.repo.nii.ac.jp/record/2003931/files/ZhangNishida2022jlamp_preprint.pdf"}, "version_id": "b9c611a7-bffe-468b-8a8c-b1ded5c323d6"}]}, "item_keyword": {"attribute_name": "キーワード", "attribute_value_mlt": [{"subitem_subject": "First-order logic", "subitem_subject_scheme": "Other"}, {"subitem_subject": "Term rewriting", "subitem_subject_scheme": "Other"}, {"subitem_subject": "Program transformation", "subitem_subject_scheme": "Other"}, {"subitem_subject": "Inductive theorem", "subitem_subject_scheme": "Other"}, {"subitem_subject": "Termination", "subitem_subject_scheme": "Other"}, {"subitem_subject": "Dependency pair", "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": "Transforming orthogonal inductive definition sets into confluent term rewrite systems", "item_titles": {"attribute_name": "タイトル", "attribute_value_mlt": [{"subitem_title": "Transforming orthogonal inductive definition sets into confluent term rewrite systems", "subitem_title_language": "en"}]}, "item_type_id": "40001", "owner": "17", "path": ["314"], "permalink_uri": "http://hdl.handle.net/2237/0002003931", "pubdate": {"attribute_name": "PubDate", "attribute_value": "2022-10-17"}, "publish_date": "2022-10-17", "publish_status": "0", "recid": "2003931", "relation": {}, "relation_version_is_last": true, "title": ["Transforming orthogonal inductive definition sets into confluent term rewrite systems"], "weko_shared_id": -1}