WEKO3
アイテム
{"_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}
Transforming orthogonal inductive definition sets into confluent term rewrite systems
http://hdl.handle.net/2237/0002003931
http://hdl.handle.net/2237/0002003931ccf6e12d-4642-42d1-bd7f-16fbe768db52
名前 / ファイル | ライセンス | アクション |
---|---|---|
ZhangNishida2022jlamp_preprint.pdf (738 KB)
Download is available from 2024/5/31.
|
|
Item type | itemtype_ver1(1) | |||||||||
---|---|---|---|---|---|---|---|---|---|---|
公開日 | 2022-10-17 | |||||||||
タイトル | ||||||||||
タイトル | Transforming orthogonal inductive definition sets into confluent term rewrite systems | |||||||||
言語 | en | |||||||||
著者 |
Zhang, Shujun
× Zhang, Shujun
× Nishida, Naoki
|
|||||||||
アクセス権 | ||||||||||
アクセス権 | embargoed access | |||||||||
アクセス権URI | http://purl.org/coar/access_right/c_f1cf | |||||||||
権利 | ||||||||||
言語 | en | |||||||||
権利情報 | © 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/ | |||||||||
キーワード | ||||||||||
主題Scheme | Other | |||||||||
主題 | First-order logic | |||||||||
キーワード | ||||||||||
主題Scheme | Other | |||||||||
主題 | Term rewriting | |||||||||
キーワード | ||||||||||
主題Scheme | Other | |||||||||
主題 | Program transformation | |||||||||
キーワード | ||||||||||
主題Scheme | Other | |||||||||
主題 | Inductive theorem | |||||||||
キーワード | ||||||||||
主題Scheme | Other | |||||||||
主題 | Termination | |||||||||
キーワード | ||||||||||
主題Scheme | Other | |||||||||
主題 | Dependency pair | |||||||||
内容記述 | ||||||||||
内容記述 | 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. | |||||||||
言語 | en | |||||||||
内容記述タイプ | Abstract | |||||||||
出版者 | ||||||||||
言語 | en | |||||||||
出版者 | Elsevier | |||||||||
言語 | ||||||||||
言語 | eng | |||||||||
資源タイプ | ||||||||||
資源タイプresource | http://purl.org/coar/resource_type/c_6501 | |||||||||
タイプ | journal article | |||||||||
出版タイプ | ||||||||||
出版タイプ | AM | |||||||||
出版タイプResource | http://purl.org/coar/version/c_ab4af688f83e57aa | |||||||||
関連情報 | ||||||||||
関連タイプ | isVersionOf | |||||||||
識別子タイプ | DOI | |||||||||
関連識別子 | https://doi.org/10.1016/j.jlamp.2022.100779 | |||||||||
収録物識別子 | ||||||||||
収録物識別子タイプ | PISSN | |||||||||
収録物識別子 | 2352-2208 | |||||||||
書誌情報 |
en : Journal of Logical and Algebraic Methods in Programming 巻 127, p. 100779, 発行日 2022-06 |
|||||||||
ファイル公開日 | ||||||||||
日付 | 2024-06-01 | |||||||||
日付タイプ | Available |