WEKO3
-
RootNode
アイテム
Argument Filterings and Usable Rules in Higher-order Rewrite Systems
https://ipsj.ixsq.nii.ac.jp/records/73760
https://ipsj.ixsq.nii.ac.jp/records/73760c19c224f-2bcc-4543-9bbe-2f5124b17a3a
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-TPRO0402002.pdf (337.7 kB)
|
Copyright (c) 2011 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Trans(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2011-03-25 | |||||||
| タイトル | ||||||||
| タイトル | Argument Filterings and Usable Rules in Higher-order Rewrite Systems | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Argument Filterings and Usable Rules in Higher-order Rewrite Systems | |||||||
| 言語 | ||||||||
| 言語 | eng | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | 通常論文 | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||
| 資源タイプ | journal article | |||||||
| 著者所属 | ||||||||
| Graduate School of Information Science, Nagoya University | ||||||||
| 著者所属 | ||||||||
| Graduate School of Information Science, Nagoya University | ||||||||
| 著者所属 | ||||||||
| INRIA, France | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Information Science, Nagoya University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Information Science, Nagoya University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| INRIA, France | ||||||||
| 著者名 |
Sho, Suzuki
Keiichirou, Kusakari
Frederic, Blanqui
× Sho, Suzuki Keiichirou, Kusakari Frederic, Blanqui
|
|||||||
| 著者名(英) |
Sho, Suzuki
Keiichirou, Kusakari
Frederic, Blanqui
× Sho, Suzuki Keiichirou, Kusakari Frederic, Blanqui
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | The static dependency pair method is a method for proving the termination of higher-order rewrite systems a la Nipkow. It combines the dependency pair method introduced for first-order rewrite systems with the notion of strong computability introduced for typed λ-calculi. Argument filterings and usable rules are two important methods of the dependency pair framework used by current state-of-the-art first-order automated termination provers. In this paper, we extend the class of higher-order systems on which the static dependency pair method can be applied. Then, we extend argument filterings and usable rules to higher-order rewriting, hence providing the basis for a powerful automated termination prover for higher-order rewrite systems. | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | The static dependency pair method is a method for proving the termination of higher-order rewrite systems a la Nipkow. It combines the dependency pair method introduced for first-order rewrite systems with the notion of strong computability introduced for typed λ-calculi. Argument filterings and usable rules are two important methods of the dependency pair framework used by current state-of-the-art first-order automated termination provers. In this paper, we extend the class of higher-order systems on which the static dependency pair method can be applied. Then, we extend argument filterings and usable rules to higher-order rewriting, hence providing the basis for a powerful automated termination prover for higher-order rewrite systems. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AA11464814 | |||||||
| 書誌情報 |
情報処理学会論文誌プログラミング（PRO） 巻 4, 号 2, p. 1-12, 発行日 2011-03-25 |
|||||||
| ISSN | ||||||||
| 収録物識別子タイプ | ISSN | |||||||
| 収録物識別子 | 1882-7802 | |||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
