ログイン
言語:

WEKO3

  • トップ
  • コミュニティ
  • ランキング
AND
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"}, "item_10_biblio_info_6": {"attribute_name": "\u66f8\u8a8c\u60c5\u5831", "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"}]}]}, "item_10_description_4": {"attribute_name": "\u6284\u9332", "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_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": "\u51fa\u7248\u8005", "attribute_value_mlt": [{"subitem_publisher": "IEICE"}]}, "item_10_rights_12": {"attribute_name": "\u6a29\u5229", "attribute_value_mlt": [{"subitem_rights": "Copyright 2005 IEICE \u8a31\u8afe\u756a\u53f7 08RB0027\u53f7"}]}, "item_10_select_15": {"attribute_name": "\u8457\u8005\u7248\u30d5\u30e9\u30b0", "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": "ISSN"}]}, "item_10_text_14": {"attribute_name": "\u30d5\u30a9\u30fc\u30de\u30c3\u30c8", "attribute_value_mlt": [{"subitem_text_value": "application/pdf"}]}, "item_creator": {"attribute_name": "\u8457\u8005", "attribute_type": "creator", "attribute_value_mlt": [{"creatorNames": [{"creatorName": "KUSAKARI, Keiichirou"}], "nameIdentifiers": [{"nameIdentifier": "22465", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "SAKAI, Masahiko"}], "nameIdentifiers": [{"nameIdentifier": "22466", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "SAKABE, Toshiki"}], "nameIdentifiers": [{"nameIdentifier": "22467", "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": "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_free", "mimetype": "application/pdf", "size": 1300000.0, "url": {"label": "E88-D_n12_2715-2726.pdf", "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": "\u30ad\u30fc\u30ef\u30fc\u30c9", "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": "\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": "Primitive Inductive Theorems Bridge Implicit Induction Methods and Inductive Theorems in Higher-Order Rewriting", "item_titles": {"attribute_name": "\u30bf\u30a4\u30c8\u30eb", "attribute_value_mlt": [{"subitem_title": "Primitive Inductive Theorems Bridge Implicit Induction Methods and Inductive Theorems in Higher-Order Rewriting"}]}, "item_type_id": "10", "owner": "1", "path": ["312/313/314"], "permalink_uri": "http://hdl.handle.net/2237/9580", "pubdate": {"attribute_name": "\u516c\u958b\u65e5", "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": null}
  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
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
著者 KUSAKARI, Keiichirou

× KUSAKARI, Keiichirou

WEKO 22465

KUSAKARI, Keiichirou

Search repository
SAKAI, Masahiko

× SAKAI, Masahiko

WEKO 22466

SAKAI, Masahiko

Search repository
SAKABE, Toshiki

× SAKABE, Toshiki

WEKO 22467

SAKABE, Toshiki

Search repository
権利
権利情報 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.
内容記述タイプ Abstract
出版者
出版者 IEICE
言語
言語 eng
資源タイプ
資源タイプresource http://purl.org/coar/resource_type/c_6501
タイプ journal article
ISSN
収録物識別子タイプ ISSN
収録物識別子 0916-8532
書誌情報 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 CiteULike Twitter Facebook Print Addthis

Cite as

Export

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

Confirm


Powered by CERN Data Centre & Invenio


Powered by CERN Data Centre & Invenio