ログイン
言語:

WEKO3

  • トップ
  • ランキング
To
lat lon distance
To

Field does not validate



インデックスリンク

インデックスツリー

メールアドレスを入力してください。

WEKO

One fine body…

WEKO

One fine body…

アイテム

{"_buckets": {"deposit": "f96885ff-152f-476c-92aa-2115b2c2fb59"}, "_deposit": {"id": "7860", "owners": [], "pid": {"revision_id": 0, "type": "depid", "value": "7860"}, "status": "published"}, "_oai": {"id": "oai:nagoya.repo.nii.ac.jp:00007860", "sets": ["314"]}, "author_link": ["22465", "22466", "22467"], "item_10_biblio_info_6": {"attribute_name": "書誌情報", "attribute_value_mlt": [{"bibliographicIssueDates": {"bibliographicIssueDate": "2005-12", "bibliographicIssueDateType": "Issued"}, "bibliographicIssueNumber": "12", "bibliographicPageEnd": "2726", "bibliographicPageStart": "2715", "bibliographicVolumeNumber": "E88-D", "bibliographic_titles": [{"bibliographic_title": "IEICE Transactions on Information and Systems", "bibliographic_titleLang": "en"}]}]}, "item_10_description_4": {"attribute_name": "抄録", "attribute_value_mlt": [{"subitem_description": "Automated reasoning of inductive theorems is considered important in program verification. To verify inductive theorems automatically, several implicit induction methods like the inductionless induction and the rewriting induction methods have been proposed. In studying inductive theorems on higher-order rewritings, we found that the class of the theorems shown by known implicit induction methods does not coincide with that of inductive theorems, and the gap between them is a barrier in developing mechanized methods for disproving inductive theorems. This paper fills this gap by introducing the notion of primitive inductive theorems, and clarifying the relation between inductive theorems and primitive inductive theorems. Based on this relation, we achieve mechanized methods for proving and disproving inductive theorems.", "subitem_description_language": "en", "subitem_description_type": "Abstract"}]}, "item_10_identifier_60": {"attribute_name": "URI", "attribute_value_mlt": [{"subitem_identifier_type": "HDL", "subitem_identifier_uri": "http://hdl.handle.net/2237/9580"}]}, "item_10_publisher_32": {"attribute_name": "出版者", "attribute_value_mlt": [{"subitem_publisher": "IEICE", "subitem_publisher_language": "ja"}]}, "item_10_rights_12": {"attribute_name": "権利", "attribute_value_mlt": [{"subitem_rights": "Copyright 2005 IEICE 許諾番号 08RB0027号", "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": "0916-8532", "subitem_source_identifier_type": "PISSN"}]}, "item_10_text_14": {"attribute_name": "フォーマット", "attribute_value_mlt": [{"subitem_text_value": "application/pdf"}]}, "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": "KUSAKARI, Keiichirou", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "22465", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "SAKAI, Masahiko", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "22466", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "SAKABE, Toshiki", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "22467", "nameIdentifierScheme": "WEKO"}]}]}, "item_files": {"attribute_name": "ファイル情報", "attribute_type": "file", "attribute_value_mlt": [{"accessrole": "open_date", "date": [{"dateType": "Available", "dateValue": "2018-02-19"}], "displaytype": "detail", "download_preview_message": "", "file_order": 0, "filename": "E88-D_n12_2715-2726.pdf", "filesize": [{"value": "1.3 MB"}], "format": "application/pdf", "future_date_message": "", "is_thumbnail": false, "licensetype": "license_note", "mimetype": "application/pdf", "size": 1300000.0, "url": {"label": "E88-D_n12_2715-2726.pdf", "objectType": "fulltext", "url": "https://nagoya.repo.nii.ac.jp/record/7860/files/E88-D_n12_2715-2726.pdf"}, "version_id": "f68428ed-9fd8-4d95-9c47-e54786958679"}]}, "item_keyword": {"attribute_name": "キーワード", "attribute_value_mlt": [{"subitem_subject": "algebraic specification", "subitem_subject_scheme": "Other"}, {"subitem_subject": "simply-typed term rewriting system", "subitem_subject_scheme": "Other"}, {"subitem_subject": "primitive inductive theorem", "subitem_subject_scheme": "Other"}, {"subitem_subject": "inductive theorem", "subitem_subject_scheme": "Other"}, {"subitem_subject": "implicit induction method", "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": "Primitive Inductive Theorems Bridge Implicit Induction Methods and Inductive Theorems in Higher-Order Rewriting", "item_titles": {"attribute_name": "タイトル", "attribute_value_mlt": [{"subitem_title": "Primitive Inductive Theorems Bridge Implicit Induction Methods and Inductive Theorems in Higher-Order Rewriting", "subitem_title_language": "en"}]}, "item_type_id": "10", "owner": "1", "path": ["314"], "permalink_uri": "http://hdl.handle.net/2237/9580", "pubdate": {"attribute_name": "PubDate", "attribute_value": "2008-03-10"}, "publish_date": "2008-03-10", "publish_status": "0", "recid": "7860", "relation": {}, "relation_version_is_last": true, "title": ["Primitive Inductive Theorems Bridge Implicit Induction Methods and Inductive Theorems in Higher-Order Rewriting"], "weko_shared_id": -1}
  1. A500 情報学部/情報学研究科・情報文化学部・情報科学研究科
  2. A500a 雑誌掲載論文
  3. 学術雑誌

Primitive Inductive Theorems Bridge Implicit Induction Methods and Inductive Theorems in Higher-Order Rewriting

http://hdl.handle.net/2237/9580
http://hdl.handle.net/2237/9580
729d6567-d065-49f5-9b5c-916d2733064e
名前 / ファイル ライセンス アクション
E88-D_n12_2715-2726.pdf E88-D_n12_2715-2726.pdf (1.3 MB)
Item type 学術雑誌論文 / Journal Article(1)
公開日 2008-03-10
タイトル
タイトル Primitive Inductive Theorems Bridge Implicit Induction Methods and Inductive Theorems in Higher-Order Rewriting
言語 en
著者 KUSAKARI, Keiichirou

× KUSAKARI, Keiichirou

WEKO 22465

en KUSAKARI, Keiichirou

Search repository
SAKAI, Masahiko

× SAKAI, Masahiko

WEKO 22466

en SAKAI, Masahiko

Search repository
SAKABE, Toshiki

× SAKABE, Toshiki

WEKO 22467

en SAKABE, Toshiki

Search repository
アクセス権
アクセス権 open access
アクセス権URI http://purl.org/coar/access_right/c_abf2
権利
言語 ja
権利情報 Copyright 2005 IEICE 許諾番号 08RB0027号
キーワード
主題Scheme Other
主題 algebraic specification
キーワード
主題Scheme Other
主題 simply-typed term rewriting system
キーワード
主題Scheme Other
主題 primitive inductive theorem
キーワード
主題Scheme Other
主題 inductive theorem
キーワード
主題Scheme Other
主題 implicit induction method
抄録
内容記述 Automated reasoning of inductive theorems is considered important in program verification. To verify inductive theorems automatically, several implicit induction methods like the inductionless induction and the rewriting induction methods have been proposed. In studying inductive theorems on higher-order rewritings, we found that the class of the theorems shown by known implicit induction methods does not coincide with that of inductive theorems, and the gap between them is a barrier in developing mechanized methods for disproving inductive theorems. This paper fills this gap by introducing the notion of primitive inductive theorems, and clarifying the relation between inductive theorems and primitive inductive theorems. Based on this relation, we achieve mechanized methods for proving and disproving inductive theorems.
言語 en
内容記述タイプ Abstract
出版者
言語 ja
出版者 IEICE
言語
言語 eng
資源タイプ
資源タイプresource http://purl.org/coar/resource_type/c_6501
タイプ journal article
出版タイプ
出版タイプ VoR
出版タイプResource http://purl.org/coar/version/c_970fb48d4fbd8a85
ISSN
収録物識別子タイプ PISSN
収録物識別子 0916-8532
書誌情報 en : IEICE Transactions on Information and Systems

巻 E88-D, 号 12, p. 2715-2726, 発行日 2005-12
フォーマット
application/pdf
著者版フラグ
値 publisher
URI
識別子 http://hdl.handle.net/2237/9580
識別子タイプ HDL
戻る
0
views
See details
Views

Versions

Ver.1 2021-03-01 20:06:46.073264
Show All versions

Share

Mendeley Twitter Facebook Print Addthis

Cite as

エクスポート

OAI-PMH
  • OAI-PMH JPCOAR
  • OAI-PMH DublinCore
  • OAI-PMH DDI
Other Formats
  • JSON
  • BIBTEX

Confirm


Powered by WEKO3


Powered by WEKO3