{"created":"2023-05-15T15:32:20.747057+00:00","id":5213,"links":{},"metadata":{"_buckets":{"deposit":"1f8de9dc-c566-4c69-b41c-a06b3ff58cc0"},"_deposit":{"created_by":17,"id":"5213","owners":[17],"pid":{"revision_id":0,"type":"depid","value":"5213"},"status":"published"},"_oai":{"id":"oai:barrel.repo.nii.ac.jp:00005213","sets":["1:628"]},"author_link":["32519","32521","32518","32520","32515"],"item_1_biblio_info_5":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicIssueDates":{"bibliographicIssueDate":"2013-11","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"11","bibliographicPageEnd":"4430","bibliographicPageStart":"4419","bibliographicVolumeNumber":"9","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":"Equivalent Transformation (ET) rules can be used to construct correct sequential and parallel programs, as they are inherently correct. One important method for making ET rules uses logical formulas. Among logical formulas, unsatisfiable conjunctions of finite atoms, each of which is represented by an atom set in this paper, are especially useful for making many ET rules that are used for constructing efficient programs. This paper proposes a method of proving unsatisfiability of an atom set based on computation by ET rules. The proposed method is recursive, in the sense that, during proving the given atom set, it may find a new atom set based on subset relation or inductive structure. Since our proposed method incorporates search based on subset and inductive relations, it can be used to prove unsatisfiability of various atom sets that cannot be proven by conventional methods. ","subitem_description_type":"Abstract"}]},"item_1_full_name_3":{"attribute_name":"著者別名","attribute_value_mlt":[{"nameIdentifiers":[{"nameIdentifier":"32521","nameIdentifierScheme":"WEKO"}],"names":[{"name":"三浦, 克宜"}]}]},"item_1_publisher_6":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"ICIC International "}]},"item_1_rights_12":{"attribute_name":"権利表記","attribute_value_mlt":[{"subitem_rights":"©2013 ICIC International "}]},"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":"13494198 ","subitem_source_identifier_type":"ISSN"}]},"item_1_subject_16":{"attribute_name":"日本十進分類法","attribute_value_mlt":[{"subitem_subject":"375 ","subitem_subject_scheme":"NDC"}]},"item_1_subject_17":{"attribute_name":"NIIサブジェクト","attribute_value_mlt":[{"subitem_subject":"メディア・コミュニケーション ","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"}],"nameIdentifiers":[{"nameIdentifier":"32515","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"Akama, Kiyoshi"}],"nameIdentifiers":[{"nameIdentifier":"32518","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"Koike, Hidekatsu"}],"nameIdentifiers":[{"nameIdentifier":"32519","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"Mabuchi, Hiroshi"}],"nameIdentifiers":[{"nameIdentifier":"32520","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":"IJICIC2013-9-11.pdf","filesize":[{"value":"687.9 kB"}],"format":"application/pdf","licensetype":"license_note","mimetype":"application/pdf","url":{"label":"IJICIC2013-9-11","url":"https://barrel.repo.nii.ac.jp/record/5213/files/IJICIC2013-9-11.pdf"},"version_id":"3ea7921e-8f7a-4c11-ae22-bae26e9bfa10"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"Unsatisability","subitem_subject_language":"en","subitem_subject_scheme":"Other"},{"subitem_subject":"Proof","subitem_subject_language":"en","subitem_subject_scheme":"Other"},{"subitem_subject":"Equivalent transformation 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":"PROOF OF UNSATISFIABILITY OF ATOM SETS BASED ON COMPUTATION BY EQUIVALENT TRANSFORMATION RULES","item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"PROOF OF UNSATISFIABILITY OF ATOM SETS BASED ON COMPUTATION BY EQUIVALENT TRANSFORMATION RULES"},{"subitem_title":"PROOF OF UNSATISFIABILITY OF ATOM SETS BASED ON COMPUTATION BY EQUIVALENT TRANSFORMATION RULES","subitem_title_language":"en"}]},"item_type_id":"1","owner":"17","path":["628"],"pubdate":{"attribute_name":"公開日","attribute_value":"2018-09-21"},"publish_date":"2018-09-21","publish_status":"0","recid":"5213","relation_version_is_last":true,"title":["PROOF OF UNSATISFIABILITY OF ATOM SETS BASED ON COMPUTATION BY EQUIVALENT TRANSFORMATION RULES"],"weko_creator_id":"17","weko_shared_id":-1},"updated":"2023-05-15T16:15:59.058594+00:00"}