ログイン 新規登録
言語:

WEKO3

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

Field does not validate



インデックスリンク

インデックスツリー

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

WEKO

One fine body…

WEKO

One fine body…

アイテム

  1. 論文誌(トランザクション)
  2. プログラミング(PRO)
  3. Vol.5
  4. No.1

書き換え帰納法における文脈探索の有効性について

https://ipsj.ixsq.nii.ac.jp/records/81559
https://ipsj.ixsq.nii.ac.jp/records/81559
b7e675ae-536d-4ad0-9ca8-4a5a75ec0335
名前 / ファイル ライセンス アクション
IPSJ-TPRO0501009.pdf IPSJ-TPRO0501009.pdf (106.5 kB)
Copyright (c) 2012 by the Information Processing Society of Japan
オープンアクセス
Item type Trans(1)
公開日 2012-03-28
タイトル
タイトル 書き換え帰納法における文脈探索の有効性について
タイトル
言語 en
タイトル Effectiveness of Context-search in Rewriting Induction
言語
言語 jpn
キーワード
主題Scheme Other
主題 発表概要
資源タイプ
資源タイプ識別子 http://purl.org/coar/resource_type/c_6501
資源タイプ journal article
著者所属
北海道大学大学院情報科学研究科
著者所属
北海道大学大学院情報科学研究科
著者所属(英)
en
Graduate School of Information Science and Technology, Hokkaido University
著者所属(英)
en
Graduate School of Information Science and Technology, Hokkaido University
著者名 佐藤, 晴彦 栗原, 正仁

× 佐藤, 晴彦 栗原, 正仁

佐藤, 晴彦
栗原, 正仁

Search repository
著者名(英) Haruhiko, Sato Masahito, Kurihara

× Haruhiko, Sato Masahito, Kurihara

en Haruhiko, Sato
Masahito, Kurihara

Search repository
論文抄録
内容記述タイプ Other
内容記述 帰納的定理とは,自然数やリストといった帰納的に定義されるデータ構造上で成り立つ命題であり,システムの正当性や安全性といった性質の検証において,帰納的定理の証明は重要となる.等式論理における帰納的定理の証明原理の1つに,Reddyによって提案された書き換え帰納法がある.書き換え帰納法に基づく証明を成功させるには,等式の向き付けや書き換え規則の適用といった非決定性を持つ推論において適切なものを選択し,帰納法の仮定や補題からなる文脈を適切に構成することが重要となるが,適切な文脈を得るための一般的な戦略を事前に定めておくことは容易ではない.本発表では,書き換え帰納法に基づく証明を網羅的な探索に基づいて自動化することを目的とし,書き換え帰納法に基づく複数の証明手続きを効率よく並列実行する多重文脈書き換え帰納法(MRIt)を提案する.提案する手続きでは書き換え帰納法に基づく複数の証明手続きの並列実行を仮想的にシミュレートし,項の書き換えや等式の展開などの基本的な推論を複数の手続きの間で共有することで効率化を図る.また,手続きは項書換え系の停止性自動証明器を利用することで,帰納法に必要な項の順序関係が存在することを保証しながら,潜在的な順序の下で可能となる推論を幅広く試みる.また,手続きが有効ないくつかの例を示し,有効性を検討する.
論文抄録(英)
内容記述タイプ Other
内容記述 Inductive theorem is a proposition which is defined on the data structure defined inductively, such as natural numbers and lists. Inductive theorem proving plays an important role in the field of formal verification of systems. The rewriting induction (RI) is a method for inductive theorem proving proposed by Reddy. In order to obtain successful proofs, it is very important to construct appropriate contexts, consisting inductive hypotheses and lemmas, in orientation of each equation and applying rewrite rules. However, it is not easy to specify general strategy for constructing appropriate contexts. In this talk, in order to automate proof search in RI by exhaustive search, we propose a new procedure, called multi-context rewriting induction, which executes several instances of the rewriting induction procedure efficiently in parallel. This procedure efficiently simulates parallel execution of rewriting induction procedures in a single process by sharing basic inferences such as reduction and expansion among simulated instances. This procedure uses automated termination checker of term rewriting systems for ensuring existence of reduction order. Finally, we show some examples for which the new procedure works effectively.
書誌レコードID
収録物識別子タイプ NCID
収録物識別子 AA11464814
書誌情報 情報処理学会論文誌プログラミング(PRO)

巻 5, 号 1, p. 30-30, 発行日 2012-03-28
ISSN
収録物識別子タイプ ISSN
収録物識別子 1882-7802
出版者
言語 ja
出版者 情報処理学会
戻る
0
views
See details
Views

Versions

Ver.1 2025-01-21 19:18:53.905506
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