{"created":"2023-05-15T15:32:20.704597+00:00","id":5212,"links":{},"metadata":{"_buckets":{"deposit":"f630271d-44d9-4404-8b83-dbd24cf513c7"},"_deposit":{"created_by":17,"id":"5212","owners":[17],"pid":{"revision_id":0,"type":"depid","value":"5212"},"status":"published"},"_oai":{"id":"oai:barrel.repo.nii.ac.jp:00005212","sets":["1:628","4"]},"author_link":["32517","32515","32516"],"item_1_biblio_info_5":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicIssueDates":{"bibliographicIssueDate":"2014-12","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"6","bibliographicPageEnd":"2009","bibliographicPageStart":"1999","bibliographicVolumeNumber":"10","bibliographic_titles":[{"bibliographic_title":"International Journal of Innovative Computing, Information and Control ","bibliographic_titleLang":"en"}]}]},"item_1_description_18":{"attribute_name":"抄録","attribute_value_mlt":[{"subitem_description":"In this paper, we propose a new method for proving the correctness of Logical Equivalences (LEs) in a newly defined class called ES. Proving the correctness of LEs is important for guaranteeing the correctness of Equivalent Transformation (ET) rules made from LEs. ET rules are useful for constructing correct sequential and parallel programs. The proposed method proves the equivalence of the declarative meaning of two definite clause sets using a bidirectional search that starts from two different points simultaneously. In the proposed method, the two definite clause sets at the starting points are transformed by ET rules. The method can generate ET rules that are essential for advancing the proof along with the general unfolding rules that are given before computing the proof. Class ES is a superclass of the classes proposed in past studies and therefore covers the LEs they contain.","subitem_description_language":"en","subitem_description_type":"Abstract"}]},"item_1_full_name_3":{"attribute_name":"著者別名","attribute_value_mlt":[{"nameIdentifiers":[{"nameIdentifier":"32517","nameIdentifierScheme":"WEKO"}],"names":[{"name":"三浦, 克宜","nameLang":"ja"}]}]},"item_1_publisher_6":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"ICIC International ","subitem_publisher_language":"en"}]},"item_1_rights_12":{"attribute_name":"権利表記","attribute_value_mlt":[{"subitem_rights":"©2014 ICIC International ","subitem_rights_language":"en"}]},"item_1_source_id_11":{"attribute_name":"書誌ID(NCID)","attribute_value_mlt":[{"subitem_source_identifier":"AA12218449","subitem_source_identifier_type":"NCID"}]},"item_1_source_id_7":{"attribute_name":"ISSN / EISSN","attribute_value_mlt":[{"subitem_source_identifier":"1349-4198","subitem_source_identifier_type":"PISSN"}]},"item_1_subject_16":{"attribute_name":"日本十進分類法","attribute_value_mlt":[{"subitem_subject":"375","subitem_subject_language":"ja","subitem_subject_scheme":"NDC"}]},"item_1_subject_17":{"attribute_name":"NIIサブジェクト","attribute_value_mlt":[{"subitem_subject":"メディア・コミュニケーション ","subitem_subject_language":"ja","subitem_subject_scheme":"Other"}]},"item_1_version_type_15":{"attribute_name":"テキストバージョン","attribute_value_mlt":[{"subitem_version_resource":"http://purl.org/coar/version/c_970fb48d4fbd8a85","subitem_version_type":"VoR"}]},"item_creator":{"attribute_name":"著者","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Miura, Katsunori","creatorNameLang":"en","creatorNameType":"Personal"}],"nameIdentifiers":[{"nameIdentifier":"32515","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"Akama, Kiyoshi","creatorNameLang":"en","creatorNameType":"Personal"}],"nameIdentifiers":[{"nameIdentifier":"32516","nameIdentifierScheme":"WEKO"}]}]},"item_files":{"attribute_name":"ファイル情報","attribute_type":"file","attribute_value_mlt":[{"accessrole":"open_date","date":[{"dateType":"Available","dateValue":"2018-09-21"}],"displaytype":"detail","filename":"IJICIC2014-10-6.pdf","filesize":[{"value":"265.7 kB"}],"format":"application/pdf","licensetype":"license_note","mimetype":"application/pdf","url":{"label":"IJICIC2014-10-6","url":"https://barrel.repo.nii.ac.jp/record/5212/files/IJICIC2014-10-6.pdf"},"version_id":"40fcec4d-70ac-4677-9eb1-8d9c6510d29a"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"Logical equivalence","subitem_subject_language":"en","subitem_subject_scheme":"Other"},{"subitem_subject":"Bidirectional search","subitem_subject_language":"en","subitem_subject_scheme":"Other"},{"subitem_subject":"Correctness","subitem_subject_language":"en","subitem_subject_scheme":"Other"},{"subitem_subject":"ET rule","subitem_subject_language":"en","subitem_subject_scheme":"Other"},{"subitem_subject":"Induction","subitem_subject_language":"en","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":"ET-BASED BIDIRECTIONAL SEARCH FOR PROVING FORMULAS IN THE CLASS ES","item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"ET-BASED BIDIRECTIONAL SEARCH FOR PROVING FORMULAS IN THE CLASS ES","subitem_title_language":"en"}]},"item_type_id":"1","owner":"17","path":["4","628"],"pubdate":{"attribute_name":"PubDate","attribute_value":"2018-09-21"},"publish_date":"2018-09-21","publish_status":"0","recid":"5212","relation_version_is_last":true,"title":["ET-BASED BIDIRECTIONAL SEARCH FOR PROVING FORMULAS IN THE CLASS ES"],"weko_creator_id":"17","weko_shared_id":-1},"updated":"2025-03-17T00:27:22.613893+00:00"}