WEKO3
AND
アイテム
{"_buckets": {"deposit": "254f06d4-f54e-41ea-8002-165618bb270f"}, "_deposit": {"id": "7952", "owners": [], "pid": {"revision_id": 0, "type": "depid", "value": "7952"}, "status": "published"}, "_oai": {"id": "oai:kitami-it.repo.nii.ac.jp:00007952", "sets": ["1:87"]}, "author_link": ["44889", "41155", "41156", "41157", "41158"], "item_1646810750418": {"attribute_name": "\u51fa\u7248\u30bf\u30a4\u30d7", "attribute_value_mlt": [{"subitem_version_resource": "http://purl.org/coar/version/c_970fb48d4fbd8a85", "subitem_version_type": "VoR"}]}, "item_3_biblio_info_186": {"attribute_name": "\u66f8\u8a8c\u60c5\u5831", "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"}]}]}, "item_3_description_184": {"attribute_name": "\u6284\u9332", "attribute_value_mlt": [{"subitem_description": "Equivalent Transformation (ET) rules can be used to construct correct se-\nquential and parallel programs, as they are inherently correct. One important method\nfor making ET rules uses logical formulas. Among logical formulas, unsatis able con-\njunctions of nite atoms, each of which is represented by an atom set in this paper, are\nespecially useful for making many ET rules that are used for constructing efficient pro-\ngrams. This paper proposes a method of proving unsatis ability of an atom set based on\ncomputation by ET rules. The proposed method is recursive, in the sense that, during\nproving the given atom set, it may nd a new atom set based on subset relation or in-\nductive structure. Since our proposed method incorporates search based on subset and\ninductive relations, it can be used to prove unsatis ability of various atom sets that can-\nnot be proven by conventional methods.", "subitem_description_type": "Abstract"}]}, "item_3_full_name_183": {"attribute_name": "\u8457\u8005\u5225\u540d", "attribute_value_mlt": [{"nameIdentifiers": [{"nameIdentifier": "44889", "nameIdentifierScheme": "WEKO"}, {"nameIdentifier": "50636587", "nameIdentifierScheme": "KAKEN", "nameIdentifierURI": "https://nrid.nii.ac.jp/ja/nrid/1000050636587 "}], "names": [{"name": "\u4e09\u6d66, \u514b\u5b9c", "nameLang": "ja"}]}]}, "item_3_link_221": {"attribute_name": "\u95a2\u9023\u30b5\u30a4\u30c8", "attribute_value_mlt": [{"subitem_link_url": "http://www.ijicic.org/contents.htm"}]}, "item_3_publisher_212": {"attribute_name": "\u51fa\u7248\u8005", "attribute_value_mlt": [{"subitem_publisher": "ICIC International"}]}, "item_3_rights_192": {"attribute_name": "\u6a29\u5229", "attribute_value_mlt": [{"subitem_rights": "c 2013 ICIC International"}]}, "item_3_select_195": {"attribute_name": "\u8457\u8005\u7248\u30d5\u30e9\u30b0", "attribute_value_mlt": [{"subitem_select_item": "publisher"}]}, "item_3_subject_196": {"attribute_name": "\u65e5\u672c\u5341\u9032\u5206\u985e\u6cd5", "attribute_value_mlt": [{"subitem_subject": "007", "subitem_subject_scheme": "NDC"}]}, "item_access_right": {"attribute_name": "\u30a2\u30af\u30bb\u30b9\u6a29", "attribute_value_mlt": [{"subitem_access_right_uri": "open access"}]}, "item_creator": {"attribute_name": "\u8457\u8005", "attribute_type": "creator", "attribute_value_mlt": [{"creatorNames": [{"creatorName": "Miura, Katsunori", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "41155", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "Akama, Kiyoshi", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "41156", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "Koike, Hidekatsu", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "41157", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "Mabuchi, Hiroshi", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "41158", "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": "2016-11-22"}], "displaytype": "detail", "download_preview_message": "", "file_order": 0, "filename": "2013.11_Proof of Unsatisfiability of Atom Sets based on Computation by Equivalent Transformation Rules.pdf", "filesize": [{"value": "146.7 kB"}], "format": "application/pdf", "future_date_message": "", "is_thumbnail": false, "licensetype": "license_note", "mimetype": "application/pdf", "size": 146700.0, "url": {"label": "2013.11_Proof of Unsatisfiability of Atom Sets based on Computation by Equivalent Transformation Rules.pdf", "url": "https://kitami-it.repo.nii.ac.jp/record/7952/files/2013.11_Proof of Unsatisfiability of Atom Sets based on Computation by Equivalent Transformation Rules.pdf"}, "version_id": "eadc7e5a-29ca-48a6-936e-b9e3289eb7bf"}]}, "item_keyword": {"attribute_name": "\u30ad\u30fc\u30ef\u30fc\u30c9", "attribute_value_mlt": [{"subitem_subject": "Unsatisability", "subitem_subject_scheme": "Other"}, {"subitem_subject": "Proof", "subitem_subject_scheme": "Other"}, {"subitem_subject": "Equivalent transformation rule", "subitem_subject_scheme": "Other"}, {"subitem_subject": "Induction", "subitem_subject_scheme": "Other"}]}, "item_language": {"attribute_name": "\u8a00\u8a9e", "attribute_value_mlt": [{"subitem_language": "eng"}]}, "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": "PROOF OF UNSATISFIABILITY OF ATOM SETS BASED ON COMPUTATION BY EQUIVALENT TRANSFORMATION RULES", "item_titles": {"attribute_name": "\u30bf\u30a4\u30c8\u30eb", "attribute_value_mlt": [{"subitem_title": "PROOF OF UNSATISFIABILITY OF ATOM SETS BASED ON COMPUTATION BY EQUIVALENT TRANSFORMATION RULES", "subitem_title_language": "en"}]}, "item_type_id": "3", "owner": "1", "path": ["1/87"], "permalink_uri": "https://kitami-it.repo.nii.ac.jp/records/7952", "pubdate": {"attribute_name": "PubDate", "attribute_value": "2015-09-03"}, "publish_date": "2015-09-03", "publish_status": "0", "recid": "7952", "relation": {}, "relation_version_is_last": true, "title": ["PROOF OF UNSATISFIABILITY OF ATOM SETS BASED ON COMPUTATION BY EQUIVALENT TRANSFORMATION RULES"], "weko_shared_id": -1}
PROOF OF UNSATISFIABILITY OF ATOM SETS BASED ON COMPUTATION BY EQUIVALENT TRANSFORMATION RULES
https://kitami-it.repo.nii.ac.jp/records/7952
c1486ccc-4f1c-4473-88f9-99ca0d78e010
名前 / ファイル | ライセンス | アクション | |
---|---|---|---|
![]() |
|
Item type | 学術雑誌論文 / Journal Article(1) | |||||
---|---|---|---|---|---|---|
公開日 | 2015-09-03 | |||||
タイトル | ||||||
言語 | en | |||||
タイトル | PROOF OF UNSATISFIABILITY OF ATOM SETS BASED ON COMPUTATION BY EQUIVALENT TRANSFORMATION RULES | |||||
言語 | ||||||
言語 | eng | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | Unsatisability | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | Proof | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | Equivalent transformation rule | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | Induction | |||||
資源タイプ | ||||||
資源 | http://purl.org/coar/resource_type/c_6501 | |||||
タイプ | journal article | |||||
アクセス権 | ||||||
アクセス権URI | open access | |||||
著者 |
Miura, Katsunori
× Miura, Katsunori× Akama, Kiyoshi× Koike, Hidekatsu× Mabuchi, Hiroshi |
|||||
著者別名 | ||||||
姓名 | ||||||
姓名 | 三浦, 克宜 | |||||
言語 | ja | |||||
抄録 | ||||||
内容記述タイプ | Abstract | |||||
内容記述 | Equivalent Transformation (ET) rules can be used to construct correct se- quential and parallel programs, as they are inherently correct. One important method for making ET rules uses logical formulas. Among logical formulas, unsatis able con- junctions of nite 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 pro- grams. This paper proposes a method of proving unsatis ability 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 nd a new atom set based on subset relation or in- ductive structure. Since our proposed method incorporates search based on subset and inductive relations, it can be used to prove unsatis ability of various atom sets that can- not be proven by conventional methods. |
|||||
書誌情報 |
International Journal of Innovative Computing, Information and Control 巻 9, 号 11, p. 4419-4430, 発行日 2013-11 |
|||||
権利 | ||||||
権利情報 | c 2013 ICIC International | |||||
出版者 | ||||||
出版者 | ICIC International | |||||
関連サイト | ||||||
URL | http://www.ijicic.org/contents.htm | |||||
著者版フラグ | ||||||
値 | publisher | |||||
出版タイプ | ||||||
出版タイプ | VoR | |||||
出版タイプResource | http://purl.org/coar/version/c_970fb48d4fbd8a85 |