WEKO3
アイテム
{"_buckets": {"deposit": "f0eec03d-5917-42f5-8073-b4bfcfe4fdd5"}, "_deposit": {"id": "19004", "owners": [], "pid": {"revision_id": 0, "type": "depid", "value": "19004"}, "status": "published"}, "_oai": {"id": "oai:nagoya.repo.nii.ac.jp:00019004", "sets": ["314"]}, "author_link": ["55428", "55429", "55430", "55431", "55432", "55433", "55434", "55435", "55436", "55437"], "item_10_alternative_title_19": {"attribute_name": "その他のタイトル", "attribute_value_mlt": [{"subitem_alternative_title": "On DPLL Transition Systems Modulo Equational Theories", "subitem_alternative_title_language": "en"}]}, "item_10_biblio_info_6": {"attribute_name": "書誌情報", "attribute_value_mlt": [{"bibliographicIssueDates": {"bibliographicIssueDate": "2010-10", "bibliographicIssueDateType": "Issued"}, "bibliographicIssueNumber": "227", "bibliographicPageEnd": "54", "bibliographicPageStart": "49", "bibliographicVolumeNumber": "110", "bibliographic_titles": [{"bibliographic_title": "電子情報通信学会技術研究報告SS, ソフトウェアサイエンス", "bibliographic_titleLang": "ja"}]}]}, "item_10_description_4": {"attribute_name": "抄録", "attribute_value_mlt": [{"subitem_description": "SMTソルバは,指定された述語理論の下で論理式の充足可能性判定を行うツールであり,配列,リスト,キューなどの多くの理論を法として,論理式の充足可能性判定を行うことができる.しかし,利用者自身が定義した理論を法とする論理式の充足可能性判定を行うのは容易ではない.なぜならば,その理論に対する決定手続きを合わせて与えることが必要であるためである.本稿では,等式理論を法とする充足可能性判定手続きを状態遷移系DPLL(R)として定式化し,その実装方式を提案する.DPLL(R)は,与えられた等式理論から項書換え系の完備化手続きを用いて決定手続きを自動的に生成し,充足可能性判定を行う.従って,利用者は等式集合を等式理論として与えるだけでよく,決定手続きを与えなくてよい. ", "subitem_description_language": "ja", "subitem_description_type": "Abstract"}, {"subitem_description": "SMT solvers are tools for deciding satisfiability of formulas under given theories such as arrays, lists, queues and so on. It is however not easy for users of SMT solvers to specify theories since the theories have to be associated with their decision procedures. In this paper, we formulate the procedure for solving the problem of satisfiability modulo an equational theory (SMET) as a state transition system DPLL(R), and propose its implementation scheme. DPLL(R) generates a decision procedure from a given equational theory and use it to solve the SMET problem. Thus, users can specify equational theories without giving decision procedures.", "subitem_description_language": "en", "subitem_description_type": "Abstract"}]}, "item_10_identifier_60": {"attribute_name": "URI", "attribute_value_mlt": [{"subitem_identifier_type": "URI", "subitem_identifier_uri": "http://ci.nii.ac.jp/naid/110008106386"}, {"subitem_identifier_type": "HDL", "subitem_identifier_uri": "http://hdl.handle.net/2237/21153"}]}, "item_10_publisher_32": {"attribute_name": "出版者", "attribute_value_mlt": [{"subitem_publisher": "一般社団法人電子情報通信学会", "subitem_publisher_language": "ja"}]}, "item_10_relation_43": {"attribute_name": "関連情報", "attribute_value_mlt": [{"subitem_relation_type": "isVersionOf", "subitem_relation_type_id": {"subitem_relation_type_id_text": "http://ci.nii.ac.jp/naid/110008106386", "subitem_relation_type_select": "URI"}}]}, "item_10_rights_12": {"attribute_name": "権利", "attribute_value_mlt": [{"subitem_rights": "(c)一般社団法人電子情報通信学会。本文データは学協会の許諾に基づきCiNiiから複製したものである", "subitem_rights_language": "ja"}]}, "item_10_select_15": {"attribute_name": "著者版フラグ", "attribute_value_mlt": [{"subitem_select_item": "publisher"}]}, "item_10_source_id_7": {"attribute_name": "ISSN", "attribute_value_mlt": [{"subitem_source_identifier": "0913-5685", "subitem_source_identifier_type": "PISSN"}]}, "item_1615787544753": {"attribute_name": "出版タイプ", "attribute_value_mlt": [{"subitem_version_resource": "http://purl.org/coar/version/c_970fb48d4fbd8a85", "subitem_version_type": "VoR"}]}, "item_access_right": {"attribute_name": "アクセス権", "attribute_value_mlt": [{"subitem_access_right": "open access", "subitem_access_right_uri": "http://purl.org/coar/access_right/c_abf2"}]}, "item_creator": {"attribute_name": "著者", "attribute_type": "creator", "attribute_value_mlt": [{"creatorNames": [{"creatorName": "馬場, 達也", "creatorNameLang": "ja"}], "nameIdentifiers": [{"nameIdentifier": "55428", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "坂部, 俊樹", "creatorNameLang": "ja"}], "nameIdentifiers": [{"nameIdentifier": "55429", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "西田, 直樹", "creatorNameLang": "ja"}], "nameIdentifiers": [{"nameIdentifier": "55430", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "草刈, 圭一朗", "creatorNameLang": "ja"}], "nameIdentifiers": [{"nameIdentifier": "55431", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "酒井, 正彦", "creatorNameLang": "ja"}], "nameIdentifiers": [{"nameIdentifier": "55432", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "BABA, Tatsuya", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "55433", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "SAKABE, Toshiki", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "55434", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "NISHIDA, Naoki", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "55435", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "KUSAKARI, Keiichirou", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "55436", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "SAKAI, Masahiko", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "55437", "nameIdentifierScheme": "WEKO"}]}]}, "item_files": {"attribute_name": "ファイル情報", "attribute_type": "file", "attribute_value_mlt": [{"accessrole": "open_date", "date": [{"dateType": "Available", "dateValue": "2018-02-21"}], "displaytype": "detail", "download_preview_message": "", "file_order": 0, "filename": "110008106386.pdf", "filesize": [{"value": "773.3 kB"}], "format": "application/pdf", "future_date_message": "", "is_thumbnail": false, "licensetype": "license_note", "mimetype": "application/pdf", "size": 773300.0, "url": {"label": "110008106386.pdf", "objectType": "fulltext", "url": "https://nagoya.repo.nii.ac.jp/record/19004/files/110008106386.pdf"}, "version_id": "18545b46-5385-4583-8b11-e8527a29be06"}]}, "item_keyword": {"attribute_name": "キーワード", "attribute_value_mlt": [{"subitem_subject": "SMTソルバ", "subitem_subject_scheme": "Other"}, {"subitem_subject": "DPLL", "subitem_subject_scheme": "Other"}, {"subitem_subject": "プログラム検証", "subitem_subject_scheme": "Other"}, {"subitem_subject": "項書換え系", "subitem_subject_scheme": "Other"}, {"subitem_subject": "SMT solver", "subitem_subject_scheme": "Other"}, {"subitem_subject": "program verification", "subitem_subject_scheme": "Other"}, {"subitem_subject": "term rewriting system", "subitem_subject_scheme": "Other"}]}, "item_language": {"attribute_name": "言語", "attribute_value_mlt": [{"subitem_language": "jpn"}]}, "item_resource_type": {"attribute_name": "資源タイプ", "attribute_value_mlt": [{"resourcetype": "journal article", "resourceuri": "http://purl.org/coar/resource_type/c_6501"}]}, "item_title": "等式理論を法とするDPLL遷移系について", "item_titles": {"attribute_name": "タイトル", "attribute_value_mlt": [{"subitem_title": "等式理論を法とするDPLL遷移系について", "subitem_title_language": "ja"}]}, "item_type_id": "10", "owner": "1", "path": ["314"], "permalink_uri": "http://hdl.handle.net/2237/21153", "pubdate": {"attribute_name": "PubDate", "attribute_value": "2015-01-28"}, "publish_date": "2015-01-28", "publish_status": "0", "recid": "19004", "relation": {}, "relation_version_is_last": true, "title": ["等式理論を法とするDPLL遷移系について"], "weko_shared_id": -1}
等式理論を法とするDPLL遷移系について
http://hdl.handle.net/2237/21153
http://hdl.handle.net/2237/211538315750a-a92f-4f6e-9f9c-71d0f9666486
名前 / ファイル | ライセンス | アクション |
---|---|---|
110008106386.pdf (773.3 kB)
|
|
Item type | 学術雑誌論文 / Journal Article(1) | |||||
---|---|---|---|---|---|---|
公開日 | 2015-01-28 | |||||
タイトル | ||||||
タイトル | 等式理論を法とするDPLL遷移系について | |||||
言語 | ja | |||||
その他のタイトル | ||||||
その他のタイトル | On DPLL Transition Systems Modulo Equational Theories | |||||
言語 | en | |||||
著者 |
馬場, 達也
× 馬場, 達也× 坂部, 俊樹× 西田, 直樹× 草刈, 圭一朗× 酒井, 正彦× BABA, Tatsuya× SAKABE, Toshiki× NISHIDA, Naoki× KUSAKARI, Keiichirou× SAKAI, Masahiko |
|||||
アクセス権 | ||||||
アクセス権 | open access | |||||
アクセス権URI | http://purl.org/coar/access_right/c_abf2 | |||||
権利 | ||||||
言語 | ja | |||||
権利情報 | (c)一般社団法人電子情報通信学会。本文データは学協会の許諾に基づきCiNiiから複製したものである | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | SMTソルバ | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | DPLL | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | プログラム検証 | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | 項書換え系 | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | SMT solver | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | program verification | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | term rewriting system | |||||
抄録 | ||||||
内容記述 | SMTソルバは,指定された述語理論の下で論理式の充足可能性判定を行うツールであり,配列,リスト,キューなどの多くの理論を法として,論理式の充足可能性判定を行うことができる.しかし,利用者自身が定義した理論を法とする論理式の充足可能性判定を行うのは容易ではない.なぜならば,その理論に対する決定手続きを合わせて与えることが必要であるためである.本稿では,等式理論を法とする充足可能性判定手続きを状態遷移系DPLL(R)として定式化し,その実装方式を提案する.DPLL(R)は,与えられた等式理論から項書換え系の完備化手続きを用いて決定手続きを自動的に生成し,充足可能性判定を行う.従って,利用者は等式集合を等式理論として与えるだけでよく,決定手続きを与えなくてよい. | |||||
言語 | ja | |||||
内容記述タイプ | Abstract | |||||
抄録 | ||||||
内容記述 | SMT solvers are tools for deciding satisfiability of formulas under given theories such as arrays, lists, queues and so on. It is however not easy for users of SMT solvers to specify theories since the theories have to be associated with their decision procedures. In this paper, we formulate the procedure for solving the problem of satisfiability modulo an equational theory (SMET) as a state transition system DPLL(R), and propose its implementation scheme. DPLL(R) generates a decision procedure from a given equational theory and use it to solve the SMET problem. Thus, users can specify equational theories without giving decision procedures. | |||||
言語 | en | |||||
内容記述タイプ | Abstract | |||||
出版者 | ||||||
言語 | ja | |||||
出版者 | 一般社団法人電子情報通信学会 | |||||
言語 | ||||||
言語 | jpn | |||||
資源タイプ | ||||||
資源タイプresource | http://purl.org/coar/resource_type/c_6501 | |||||
タイプ | journal article | |||||
出版タイプ | ||||||
出版タイプ | VoR | |||||
出版タイプResource | http://purl.org/coar/version/c_970fb48d4fbd8a85 | |||||
関連情報 | ||||||
関連タイプ | isVersionOf | |||||
識別子タイプ | URI | |||||
関連識別子 | http://ci.nii.ac.jp/naid/110008106386 | |||||
ISSN | ||||||
収録物識別子タイプ | PISSN | |||||
収録物識別子 | 0913-5685 | |||||
書誌情報 |
ja : 電子情報通信学会技術研究報告SS, ソフトウェアサイエンス 巻 110, 号 227, p. 49-54, 発行日 2010-10 |
|||||
著者版フラグ | ||||||
値 | publisher | |||||
URI | ||||||
識別子 | http://ci.nii.ac.jp/naid/110008106386 | |||||
識別子タイプ | URI | |||||
URI | ||||||
識別子 | http://hdl.handle.net/2237/21153 | |||||
識別子タイプ | HDL |